diff options
48 files changed, 3477 insertions, 708 deletions
@@ -2558,10 +2558,6 @@ SOURCE=.\src\aig\fra\fra.h # End Source File # Begin Source File -SOURCE=.\src\aig\fra\fraAnd.c -# End Source File -# Begin Source File - SOURCE=.\src\aig\fra\fraClass.c # End Source File # Begin Source File @@ -2574,6 +2570,10 @@ SOURCE=.\src\aig\fra\fraCore.c # End Source File # Begin Source File +SOURCE=.\src\aig\fra\fraDfs.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\fra\fraMan.c # End Source File # Begin Source File @@ -2758,6 +2758,18 @@ SOURCE=.\src\aig\aig\aigOper.c # End Source File # Begin Source File +SOURCE=.\src\aig\aig\aigOrder.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\aig\aigPart.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\aig\aigRepr.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\aig\aigSeq.c # End Source File # Begin Source File diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 8c9400be..230c354f 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -106,6 +106,16 @@ struct Aig_Man_t_ int nBufReplaces; // the number of times replacement led to a buffer int nBufFixes; // the number of times buffers were propagated int nBufMax; // the maximum number of buffers during computation + // topological order + unsigned * pOrderData; + int nOrderAlloc; + int iPrev; + int iNext; + int nAndTotal; + int nAndPrev; + // representatives + Aig_Obj_t ** pRepr; + int nReprAlloc; // various data members Aig_MmFixed_t * pMemObjs; // memory manager for objects Vec_Int_t * vLevelR; // the reverse level of the nodes @@ -113,6 +123,7 @@ struct Aig_Man_t_ void * pData; // the temporary data int nTravIds; // the current traversal ID int fCatchExor; // enables EXOR nodes + Aig_Obj_t ** pReprs; // linked list of equivalent nodes (when choices are used) // timing statistics int time1; int time2; @@ -124,6 +135,7 @@ struct Aig_Man_t_ #define AIG_MIN(a,b) (((a) < (b))? (a) : (b)) #define AIG_MAX(a,b) (((a) > (b))? (a) : (b)) +#define AIG_ABS(a) (((a) >= 0)? (a) :-(a)) #define AIG_INFINITY (100000000) #ifndef PRT @@ -197,7 +209,7 @@ static inline Aig_Obj_t * Aig_ObjChild0( Aig_Obj_t * pObj ) { return pObj- static inline Aig_Obj_t * Aig_ObjChild1( Aig_Obj_t * pObj ) { return pObj->pFanin1; } static inline Aig_Obj_t * Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; } static inline Aig_Obj_t * Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; } -static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { return pObj->nRefs; } +static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { return pObj->Level; } static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; } static inline int Aig_ObjFaninPhase( Aig_Obj_t * pObj ) { return pObj? Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) : 0; } static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj, 0, sizeof(Aig_Obj_t) ); } @@ -277,6 +289,11 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry ) // 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++ ) +// iterator over the nodes in the topological order +#define Aig_ManForEachNodeInOrder( p, pObj ) \ + for ( assert(p->pOrderData), p->iPrev = 0, p->iNext = p->pOrderData[1]; \ + p->iNext && (((pObj) = Aig_ManObj(p, p->iNext)), 1); \ + p->iNext = p->pOrderData[2*p->iPrev+1] ) // 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]; } @@ -296,22 +313,25 @@ extern int Aig_ManCheck( Aig_Man_t * p ); /*=== aigDfs.c ==========================================================*/ extern Vec_Ptr_t * Aig_ManDfs( 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_ManCountLevels( Aig_Man_t * p ); 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 ); +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 ); /*=== 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 ); -extern void Aig_ManCreateFanout( Aig_Man_t * p ); -extern void Aig_ManDeleteFanout( Aig_Man_t * p ); +extern void Aig_ManFanoutStart( Aig_Man_t * p ); +extern void Aig_ManFanoutStop( Aig_Man_t * p ); /*=== aigMan.c ==========================================================*/ -extern Aig_Man_t * Aig_ManStart(); +extern Aig_Man_t * Aig_ManStart( int nNodesMax ); extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ); +extern Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes ); extern void Aig_ManStop( Aig_Man_t * p ); extern int Aig_ManCleanup( Aig_Man_t * p ); extern void Aig_ManPrintStats( Aig_Man_t * p ); @@ -345,9 +365,25 @@ extern Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 ) extern Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 ); extern Aig_Obj_t * Aig_Maj( Aig_Man_t * p, Aig_Obj_t * pA, Aig_Obj_t * pB, Aig_Obj_t * pC ); extern Aig_Obj_t * Aig_Miter( Aig_Man_t * p, Vec_Ptr_t * vPairs ); +extern Aig_Obj_t * Aig_MiterTwo( Aig_Man_t * p, Vec_Ptr_t * vNodes1, Vec_Ptr_t * vNodes2 ); extern Aig_Obj_t * Aig_CreateAnd( Aig_Man_t * p, int nVars ); extern Aig_Obj_t * Aig_CreateOr( Aig_Man_t * p, int nVars ); extern Aig_Obj_t * Aig_CreateExor( Aig_Man_t * p, int nVars ); +/*=== aigOrder.c =========================================================*/ +extern void Aig_ManOrderStart( Aig_Man_t * p ); +extern void Aig_ManOrderStop( Aig_Man_t * p ); +extern void Aig_ObjOrderInsert( Aig_Man_t * p, int ObjId ); +extern void Aig_ObjOrderRemove( Aig_Man_t * p, int ObjId ); +extern void Aig_ObjOrderAdvance( Aig_Man_t * p ); +/*=== aigPart.c =========================================================*/ +extern Vec_Vec_t * Aig_ManSupports( Aig_Man_t * pMan ); +extern Vec_Vec_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Vec_t ** pvPartSupps ); +extern Vec_Vec_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize ); +/*=== aigRepr.c =========================================================*/ +extern void Aig_ManReprStart( Aig_Man_t * p, int nIdMax ); +extern void Aig_ManReprStop( Aig_Man_t * p ); +extern void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p ); +extern Aig_Man_t * Aig_ManCreateChoices( Aig_Man_t * p ); /*=== aigSeq.c ========================================================*/ extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits ); /*=== aigTable.c ========================================================*/ @@ -358,11 +394,14 @@ extern void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj ); extern int Aig_TableCountEntries( Aig_Man_t * p ); extern void Aig_TableProfile( Aig_Man_t * p ); /*=== aigTiming.c ========================================================*/ +extern void Aig_ObjClearReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj ); extern int Aig_ObjRequiredLevel( Aig_Man_t * p, Aig_Obj_t * pObj ); extern void Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIncrease ); 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 ); +extern void Aig_ManVerifyLevel( Aig_Man_t * p ); +extern void Aig_ManVerifyReverseLevel( Aig_Man_t * p ); /*=== 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 =========================================================*/ @@ -370,6 +409,8 @@ 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_ManCleanMarkA( Aig_Man_t * p ); +extern void Aig_ManCleanMarkB( 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 ); diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index 62900bb5..a9d3d860 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -41,9 +41,9 @@ ***********************************************************************/ void Aig_ManDfs_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) { - assert( !Aig_IsComplement(pObj) ); if ( pObj == NULL ) return; + assert( !Aig_IsComplement(pObj) ); if ( Aig_ObjIsTravIdCurrent(p, pObj) ) return; assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) ); @@ -119,6 +119,62 @@ Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes ) /**Function************************************************************* + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManDfsChoices_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + if ( pObj == NULL ) + return; + assert( !Aig_IsComplement(pObj) ); + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + assert( Aig_ObjIsNode(pObj) ); + Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes ); + Aig_ManDfsChoices_rec( p, Aig_ObjFanin1(pObj), vNodes ); + Aig_ManDfsChoices_rec( p, p->pReprs[pObj->Id], 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.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i; + assert( p->pReprs != NULL ); + 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_ManForEachPo( p, pObj, i ) + Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes ); + return vNodes; +} + +/**Function************************************************************* + Synopsis [Collects internal nodes in the reverse DFS order.] Description [] @@ -444,7 +500,7 @@ Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, in SeeAlso [] ***********************************************************************/ -void Aig_ManCollectCut_rec( Aig_Obj_t * pNode, Vec_Ptr_t * vNodes ) +void Aig_ObjCollectCut_rec( Aig_Obj_t * pNode, Vec_Ptr_t * vNodes ) { // Aig_Obj_t * pFan0 = Aig_ObjFanin0(pNode); // Aig_Obj_t * pFan1 = Aig_ObjFanin1(pNode); @@ -452,8 +508,8 @@ void Aig_ManCollectCut_rec( Aig_Obj_t * pNode, Vec_Ptr_t * vNodes ) return; pNode->fMarkA = 1; assert( Aig_ObjIsNode(pNode) ); - Aig_ManCollectCut_rec( Aig_ObjFanin0(pNode), vNodes ); - Aig_ManCollectCut_rec( Aig_ObjFanin1(pNode), vNodes ); + Aig_ObjCollectCut_rec( Aig_ObjFanin0(pNode), vNodes ); + Aig_ObjCollectCut_rec( Aig_ObjFanin1(pNode), vNodes ); Vec_PtrPush( vNodes, pNode ); //printf( "added %d ", pNode->Id ); } @@ -469,7 +525,7 @@ void Aig_ManCollectCut_rec( Aig_Obj_t * pNode, Vec_Ptr_t * vNodes ) SeeAlso [] ***********************************************************************/ -void Aig_ManCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes ) +void Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes ) { Aig_Obj_t * pObj; int i; @@ -483,7 +539,7 @@ void Aig_ManCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNod } //printf( "\n" ); // collect and mark the nodes - Aig_ManCollectCut_rec( pRoot, vNodes ); + Aig_ObjCollectCut_rec( pRoot, vNodes ); // clean the nodes Vec_PtrForEachEntry( vNodes, pObj, i ) pObj->fMarkA = 0; @@ -491,6 +547,83 @@ void Aig_ManCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNod pObj->fMarkA = 0; } + +/**Function************************************************************* + + Synopsis [Collects the nodes of the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ObjCollectSuper_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper ) +{ + int RetValue1, RetValue2, i; + // check if the node is visited + if ( Aig_Regular(pObj)->fMarkA ) + { + // check if the node occurs in the same polarity + for ( i = 0; i < vSuper->nSize; i++ ) + if ( vSuper->pArray[i] == pObj ) + return 1; + // check if the node is present in the opposite polarity + for ( i = 0; i < vSuper->nSize; i++ ) + if ( vSuper->pArray[i] == Aig_Not(pObj) ) + return -1; + assert( 0 ); + return 0; + } + // if the new node is complemented or a PI, another gate begins + if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1) ) + { + Vec_PtrPush( vSuper, pObj ); + Aig_Regular(pObj)->fMarkA = 1; + return 0; + } + assert( !Aig_IsComplement(pObj) ); + assert( Aig_ObjIsNode(pObj) ); + // go through the branches + RetValue1 = Aig_ObjCollectSuper_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper ); + RetValue2 = Aig_ObjCollectSuper_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper ); + if ( RetValue1 == -1 || RetValue2 == -1 ) + return -1; + // return 1 if at least one branch has a duplicate + return RetValue1 || RetValue2; +} + +/**Function************************************************************* + + Synopsis [Collects the nodes of the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper ) +{ + int RetValue, i; + assert( !Aig_IsComplement(pObj) ); + assert( Aig_ObjIsNode(pObj) ); + // collect the nodes in the implication supergate + Vec_PtrClear( vSuper ); + RetValue = Aig_ObjCollectSuper_rec( pObj, pObj, vSuper ); + assert( Vec_PtrSize(vSuper) > 1 ); + // unmark the visited nodes + Vec_PtrForEachEntry( vSuper, pObj, i ) + Aig_Regular(pObj)->fMarkA = 0; + // if we found the node and its complement in the same implication supergate, + // return empty set of nodes (meaning that we should use constant-0 node) + if ( RetValue == -1 ) + vSuper->nSize = 0; + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigFanout.c b/src/aig/aig/aigFanout.c index e7d5f216..9aff0fd5 100644 --- a/src/aig/aig/aigFanout.c +++ b/src/aig/aig/aigFanout.c @@ -39,6 +39,56 @@ static inline int * Aig_FanoutNext( int * pData, int iFan ) { return pData + 5 /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Create fanout for all objects in the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManFanoutStart( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + assert( Aig_ManBufNum(p) == 0 ); + // allocate fanout datastructure + assert( p->pFanData == NULL ); + p->nFansAlloc = 2 * Aig_ManObjIdMax(p); + if ( p->nFansAlloc < (1<<12) ) + p->nFansAlloc = (1<<12); + p->pFanData = ALLOC( int, 5 * p->nFansAlloc ); + memset( p->pFanData, 0, sizeof(int) * 5 * p->nFansAlloc ); + // add fanouts for all objects + Aig_ManForEachObj( p, pObj, i ) + { + if ( Aig_ObjChild0(pObj) ) + Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj ); + if ( Aig_ObjChild1(pObj) ) + Aig_ObjAddFanout( p, Aig_ObjFanin1(pObj), pObj ); + } +} + +/**Function************************************************************* + + Synopsis [Deletes fanout for all objects in the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManFanoutStop( Aig_Man_t * p ) +{ + assert( p->pFanData != NULL ); + FREE( p->pFanData ); + p->nFansAlloc = 0; +} /**Function************************************************************* @@ -132,56 +182,6 @@ void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout ) *pNextC = 0; } -/**Function************************************************************* - - Synopsis [Create fanout for all objects in the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Aig_ManCreateFanout( Aig_Man_t * p ) -{ - Aig_Obj_t * pObj; - int i; - // allocate fanout datastructure - assert( p->pFanData == NULL ); - p->nFansAlloc = 2 * Aig_ManObjIdMax(p); - if ( p->nFansAlloc < (1<<12) ) - p->nFansAlloc = (1<<12); - p->pFanData = ALLOC( int, 5 * p->nFansAlloc ); - memset( p->pFanData, 0, sizeof(int) * 5 * p->nFansAlloc ); - // add fanouts for all objects - Aig_ManForEachObj( p, pObj, i ) - { - if ( Aig_ObjChild0(pObj) ) - Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj ); - if ( Aig_ObjChild1(pObj) ) - Aig_ObjAddFanout( p, Aig_ObjFanin1(pObj), pObj ); - } -} - -/**Function************************************************************* - - Synopsis [Deletes fanout for all objects in the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Aig_ManDeleteFanout( Aig_Man_t * p ) -{ - assert( p->pFanData != NULL ); - FREE( p->pFanData ); - p->nFansAlloc = 0; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 562260d3..b235119f 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -153,11 +153,15 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) { 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 ) Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) ); // check the resulting network if ( !Aig_ManCheck(pNew) ) printf( "Aig_ManDup(): The check has failed.\n" ); @@ -166,6 +170,45 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) /**Function************************************************************* + Synopsis [Extracts the miter composed of XOR of the two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i; + assert( nNodes == 2 ); + // create the new manager + pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); + // create the PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePi(pNew); + // dump the nodes + for ( i = 0; i < nNodes; i++ ) + Aig_ManDup_rec( pNew, p, ppNodes[i] ); + // construct the EXOR + pObj = Aig_Exor( pNew, ppNodes[0]->pData, ppNodes[1]->pData ); + pObj = Aig_NotCond( pObj, Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) ); + // add the PO + Aig_ObjCreatePo( pNew, pObj ); + // check the resulting network + if ( !Aig_ManCheck(pNew) ) + printf( "Aig_ManDup(): The check has failed.\n" ); + return pNew; +} + + +/**Function************************************************************* + Synopsis [Stops the AIG manager.] Description [] @@ -184,7 +227,7 @@ void Aig_ManStop( Aig_Man_t * p ) if ( p->time2 ) { PRT( "time2", p->time2 ); } // delete fanout if ( p->pFanData ) - Aig_ManDeleteFanout( p ); + Aig_ManFanoutStop( p ); // make sure the nodes have clean marks Aig_ManForEachObj( p, pObj, i ) assert( !pObj->fMarkA && !pObj->fMarkB ); @@ -196,6 +239,7 @@ void Aig_ManStop( Aig_Man_t * p ) if ( p->vBufs ) Vec_PtrFree( p->vBufs ); if ( p->vLevelR ) Vec_IntFree( p->vLevelR ); if ( p->vLevels ) Vec_VecFree( p->vLevels ); + FREE( p->pReprs ); free( p->pTable ); free( p ); } diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c index f2296e01..a017ff2d 100644 --- a/src/aig/aig/aigObj.c +++ b/src/aig/aig/aigObj.c @@ -139,6 +139,9 @@ void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj // add the node to the structural hash table if ( Aig_ObjIsHash(pObj) ) Aig_TableInsert( p, pObj ); + // add the node to the dynamically updated topological order + if ( p->pOrderData && Aig_ObjIsNode(pObj) ) + Aig_ObjOrderInsert( p, pObj->Id ); } /**Function************************************************************* @@ -174,6 +177,9 @@ void Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj ) // add the first fanin pObj->pFanin0 = NULL; pObj->pFanin1 = NULL; + // remove the node from the dynamically updated topological order + if ( p->pOrderData && Aig_ObjIsNode(pObj) ) + Aig_ObjOrderRemove( p, pObj->Id ); } /**Function************************************************************* @@ -243,6 +249,7 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew { Aig_Obj_t * pFaninOld; assert( !Aig_IsComplement(pObj) ); + assert( Aig_ObjIsPo(pObj) ); pFaninOld = Aig_ObjFanin0(pObj); // decrement ref and remove fanout if ( p->pFanData ) @@ -386,7 +393,10 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in Aig_ManUpdateLevel( p, pObjOld ); } if ( fUpdateLevel ) + { + Aig_ObjClearReverseLevel( p, pObjOld ); Aig_ManUpdateReverseLevel( p, pObjOld ); + } } p->nObjs[pObjOld->Type]++; // store buffers if fanout is allocated diff --git a/src/aig/aig/aigOper.c b/src/aig/aig/aigOper.c index 55ab5862..d13d4bed 100644 --- a/src/aig/aig/aigOper.c +++ b/src/aig/aig/aigOper.c @@ -352,7 +352,6 @@ Aig_Obj_t * Aig_Miter( Aig_Man_t * p, Vec_Ptr_t * vPairs ) int i; assert( vPairs->nSize > 0 ); assert( vPairs->nSize % 2 == 0 ); - // go through the cubes of the node's SOP for ( i = 0; i < vPairs->nSize; i += 2 ) vPairs->pArray[i/2] = Aig_Not( Aig_Exor( p, vPairs->pArray[i], vPairs->pArray[i+1] ) ); vPairs->nSize = vPairs->nSize/2; @@ -361,6 +360,27 @@ Aig_Obj_t * Aig_Miter( Aig_Man_t * p, Vec_Ptr_t * vPairs ) /**Function************************************************************* + Synopsis [Implements the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Aig_MiterTwo( Aig_Man_t * p, Vec_Ptr_t * vNodes1, Vec_Ptr_t * vNodes2 ) +{ + int i; + assert( vNodes1->nSize > 0 && vNodes1->nSize > 0 ); + assert( vNodes1->nSize == vNodes2->nSize ); + for ( i = 0; i < vNodes1->nSize; i++ ) + vNodes1->pArray[i] = Aig_Not( Aig_Exor( p, vNodes1->pArray[i], vNodes2->pArray[i] ) ); + return Aig_Not( Aig_Multi_rec( p, (Aig_Obj_t **)vNodes1->pArray, vNodes1->nSize, AIG_OBJ_AND ) ); +} + +/**Function************************************************************* + Synopsis [Creates AND function with nVars inputs.] Description [] diff --git a/src/aig/aig/aigOrder.c b/src/aig/aig/aigOrder.c new file mode 100644 index 00000000..8aef67c8 --- /dev/null +++ b/src/aig/aig/aigOrder.c @@ -0,0 +1,171 @@ +/**CFile**************************************************************** + + FileName [aigOrder.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Dynamically updated topological order.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigOrder.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Initializes the order datastructure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManOrderStart( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + assert( Aig_ManBufNum(p) == 0 ); + // allocate order datastructure + assert( p->pOrderData == NULL ); + p->nOrderAlloc = 2 * Aig_ManObjIdMax(p); + if ( p->nOrderAlloc < (1<<12) ) + p->nOrderAlloc = (1<<12); + p->pOrderData = ALLOC( unsigned, 2 * p->nOrderAlloc ); + memset( p->pOrderData, 0xFF, sizeof(unsigned) * 2 * p->nOrderAlloc ); + // add the constant node + p->pOrderData[0] = p->pOrderData[1] = 0; + p->iPrev = p->iNext = 0; + // add the internal nodes + Aig_ManForEachNode( p, pObj, i ) + Aig_ObjOrderInsert( p, pObj->Id ); +} + +/**Function************************************************************* + + Synopsis [Deletes the order datastructure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManOrderStop( Aig_Man_t * p ) +{ + assert( p->pOrderData ); + FREE( p->pOrderData ); + p->nOrderAlloc = 0; + p->iPrev = p->iNext = 0; +} + +/**Function************************************************************* + + Synopsis [Inserts an entry before iNext.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ObjOrderInsert( Aig_Man_t * p, int ObjId ) +{ + int iPrev; + assert( ObjId != 0 ); + assert( Aig_ObjIsNode( Aig_ManObj(p, ObjId) ) ); + if ( ObjId >= p->nOrderAlloc ) + { + int nOrderAlloc = 2 * ObjId; + p->pOrderData = REALLOC( unsigned, p->pOrderData, 2 * nOrderAlloc ); + memset( p->pOrderData + 2 * p->nOrderAlloc, 0xFF, sizeof(unsigned) * 2 * (nOrderAlloc - p->nOrderAlloc) ); + p->nOrderAlloc = nOrderAlloc; + } + assert( p->pOrderData[2*ObjId] == 0xFFFFFFFF ); // prev + assert( p->pOrderData[2*ObjId+1] == 0xFFFFFFFF ); // next + iPrev = p->pOrderData[2*p->iNext]; + assert( p->pOrderData[2*iPrev+1] == (unsigned)p->iNext ); + p->pOrderData[2*ObjId] = iPrev; + p->pOrderData[2*iPrev+1] = ObjId; + p->pOrderData[2*p->iNext] = ObjId; + p->pOrderData[2*ObjId+1] = p->iNext; + p->nAndTotal++; +} + +/**Function************************************************************* + + Synopsis [Removes the entry.] + + Description [If iPrev is removed, it slides backward. + If iNext is removed, it slides forward.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ObjOrderRemove( Aig_Man_t * p, int ObjId ) +{ + int iPrev, iNext; + assert( ObjId != 0 ); + assert( Aig_ObjIsNode( Aig_ManObj(p, ObjId) ) ); + iPrev = p->pOrderData[2*ObjId]; + iNext = p->pOrderData[2*ObjId+1]; + p->pOrderData[2*ObjId] = 0xFFFFFFFF; + p->pOrderData[2*ObjId+1] = 0xFFFFFFFF; + p->pOrderData[2*iNext] = iPrev; + p->pOrderData[2*iPrev+1] = iNext; + if ( p->iPrev == ObjId ) + { + p->nAndPrev--; + p->iPrev = iPrev; + } + if ( p->iNext == ObjId ) + p->iNext = iNext; + p->nAndTotal--; +} + +/**Function************************************************************* + + Synopsis [Advances the order forward.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ObjOrderAdvance( Aig_Man_t * p ) +{ + assert( p->pOrderData ); + assert( p->pOrderData[2*p->iPrev+1] == (unsigned)p->iNext ); + p->iPrev = p->iNext; + p->nAndPrev++; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c new file mode 100644 index 00000000..371e8773 --- /dev/null +++ b/src/aig/aig/aigPart.c @@ -0,0 +1,928 @@ +/**CFile**************************************************************** + + FileName [aigPart.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [AIG partitioning package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigPart.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Part_Man_t_ Part_Man_t; +struct Part_Man_t_ +{ + int nChunkSize; // the size of one chunk of memory (~1 Mb) + int nStepSize; // the step size in saving memory (~64 bytes) + char * pFreeBuf; // the pointer to free memory + int nFreeSize; // the size of remaining free memory + Vec_Ptr_t * vMemory; // the memory allocated + Vec_Ptr_t * vFree; // the vector of free pieces of memory +}; + +typedef struct Part_One_t_ Part_One_t; +struct Part_One_t_ +{ + int nRefs; // the number of references + int nOuts; // the number of outputs + int nOutsAlloc; // the array size + int pOuts[0]; // the array of outputs +}; + +static inline int Part_SizeType( int nSize, int nStepSize ) { return nSize / nStepSize + ((nSize % nStepSize) > 0); } +static inline char * Part_OneNext( char * pPart ) { return *((char **)pPart); } +static inline void Part_OneSetNext( char * pPart, char * pNext ) { *((char **)pPart) = pNext; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Start the memory manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Part_Man_t * Part_ManStart( int nChunkSize, int nStepSize ) +{ + Part_Man_t * p; + p = ALLOC( Part_Man_t, 1 ); + memset( p, 0, sizeof(Part_Man_t) ); + p->nChunkSize = nChunkSize; + p->nStepSize = nStepSize; + p->vMemory = Vec_PtrAlloc( 1000 ); + p->vFree = Vec_PtrAlloc( 1000 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the memory manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Part_ManStop( Part_Man_t * p ) +{ + void * pMemory; + int i; + Vec_PtrForEachEntry( p->vMemory, pMemory, i ) + free( pMemory ); + Vec_PtrFree( p->vMemory ); + Vec_PtrFree( p->vFree ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Fetches the memory entry of the given size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Part_ManFetch( Part_Man_t * p, int nSize ) +{ + int Type, nSizeReal; + char * pMemory; + assert( nSize > 0 ); + Type = Part_SizeType( nSize, p->nStepSize ); + Vec_PtrFillExtra( p->vFree, Type + 1, NULL ); + if ( pMemory = Vec_PtrEntry( p->vFree, Type ) ) + { + Vec_PtrWriteEntry( p->vFree, Type, Part_OneNext(pMemory) ); + return pMemory; + } + nSizeReal = p->nStepSize * Type; + if ( p->nFreeSize < nSizeReal ) + { + p->pFreeBuf = ALLOC( char, p->nChunkSize ); + p->nFreeSize = p->nChunkSize; + Vec_PtrPush( p->vMemory, p->pFreeBuf ); + } + assert( p->nFreeSize >= nSizeReal ); + pMemory = p->pFreeBuf; + p->pFreeBuf += nSizeReal; + p->nFreeSize -= nSizeReal; + return pMemory; +} + +/**Function************************************************************* + + Synopsis [Recycles the memory entry of the given size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Part_ManRecycle( Part_Man_t * p, char * pMemory, int nSize ) +{ + int Type; + Type = Part_SizeType( nSize, p->nStepSize ); + Vec_PtrFillExtra( p->vFree, Type + 1, NULL ); + Part_OneSetNext( pMemory, Vec_PtrEntry(p->vFree, Type) ); + Vec_PtrWriteEntry( p->vFree, Type, pMemory ); +} + +/**Function************************************************************* + + Synopsis [Fetches the memory entry of the given size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Part_One_t * Part_ManFetchEntry( Part_Man_t * p, int nWords, int nRefs ) +{ + Part_One_t * pPart; + pPart = (Part_One_t *)Part_ManFetch( p, sizeof(Part_One_t) + sizeof(int) * nWords ); + pPart->nRefs = nRefs; + pPart->nOuts = 0; + pPart->nOutsAlloc = nWords; + return pPart; +} + +/**Function************************************************************* + + Synopsis [Recycles the memory entry of the given size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Part_ManRecycleEntry( Part_Man_t * p, Part_One_t * pEntry ) +{ + assert( pEntry->nOuts <= pEntry->nOutsAlloc ); + assert( pEntry->nOuts >= pEntry->nOutsAlloc/2 ); + Part_ManRecycle( p, (char *)pEntry, sizeof(Part_One_t) + sizeof(int) * pEntry->nOutsAlloc ); +} + +/**Function************************************************************* + + Synopsis [Merges two entries.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Part_One_t * Part_ManMergeEntry( Part_Man_t * pMan, Part_One_t * p1, Part_One_t * p2, int nRefs ) +{ + Part_One_t * p = Part_ManFetchEntry( pMan, p1->nOuts + p2->nOuts, nRefs ); + int * pBeg1 = p1->pOuts; + int * pBeg2 = p2->pOuts; + int * pBeg = p->pOuts; + int * pEnd1 = p1->pOuts + p1->nOuts; + int * pEnd2 = p2->pOuts + p2->nOuts; + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + if ( *pBeg1 == *pBeg2 ) + *pBeg++ = *pBeg1++, pBeg2++; + else if ( *pBeg1 < *pBeg2 ) + *pBeg++ = *pBeg1++; + else + *pBeg++ = *pBeg2++; + } + while ( pBeg1 < pEnd1 ) + *pBeg++ = *pBeg1++; + while ( pBeg2 < pEnd2 ) + *pBeg++ = *pBeg2++; + p->nOuts = pBeg - p->pOuts; + assert( p->nOuts <= p->nOutsAlloc ); + assert( p->nOuts >= p1->nOuts ); + assert( p->nOuts >= p2->nOuts ); + return p; +} + +/**Function************************************************************* + + Synopsis [Tranfers the entry.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Part_ManTransferEntry( Part_One_t * p ) +{ + Vec_Int_t * vSupp; + int i; + vSupp = Vec_IntAlloc( p->nOuts ); + for ( i = 0; i < p->nOuts; i++ ) + Vec_IntPush( vSupp, p->pOuts[i] ); + return vSupp; +} + +/**Function************************************************************* + + Synopsis [Computes supports of the POs in the multi-output AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * Aig_ManSupports( Aig_Man_t * pMan ) +{ + Vec_Vec_t * vSupps; + Vec_Int_t * vSupp; + Part_Man_t * p; + Part_One_t * pPart0, * pPart1; + Aig_Obj_t * pObj; + int i, iIns = 0, iOut = 0; + // start the support computation manager + p = Part_ManStart( 1 << 20, 1 << 6 ); + // consider objects in the topological order + vSupps = Vec_VecAlloc( Aig_ManPoNum(pMan) ); + Aig_ManCleanData(pMan); + Aig_ManForEachObj( pMan, pObj, i ) + { + if ( Aig_ObjIsNode(pObj) ) + { + pPart0 = Aig_ObjFanin0(pObj)->pData; + pPart1 = Aig_ObjFanin1(pObj)->pData; + pObj->pData = Part_ManMergeEntry( p, pPart0, pPart1, pObj->nRefs ); + assert( pPart0->nRefs > 0 ); + if ( --pPart0->nRefs == 0 ) + Part_ManRecycleEntry( p, pPart0 ); + assert( pPart1->nRefs > 0 ); + if ( --pPart1->nRefs == 0 ) + Part_ManRecycleEntry( p, pPart1 ); + continue; + } + if ( Aig_ObjIsPo(pObj) ) + { + pPart0 = Aig_ObjFanin0(pObj)->pData; + vSupp = Part_ManTransferEntry(pPart0); + Vec_IntPush( vSupp, iOut++ ); + Vec_PtrPush( (Vec_Ptr_t *)vSupps, vSupp ); + assert( pPart0->nRefs > 0 ); + if ( --pPart0->nRefs == 0 ) + Part_ManRecycleEntry( p, pPart0 ); + continue; + } + if ( Aig_ObjIsPi(pObj) ) + { + if ( pObj->nRefs ) + { + pPart0 = Part_ManFetchEntry( p, 1, pObj->nRefs ); + pPart0->pOuts[ pPart0->nOuts++ ] = iIns++; + pObj->pData = pPart0; + } + continue; + } + if ( Aig_ObjIsConst1(pObj) ) + { + if ( pObj->nRefs ) + pObj->pData = Part_ManFetchEntry( p, 0, pObj->nRefs ); + continue; + } + assert( 0 ); + } +printf( "Memory usage = %d Mb.\n", Vec_PtrSize(p->vMemory) * p->nChunkSize / (1<<20) ); + Part_ManStop( p ); + // sort supports by size + Vec_VecSort( vSupps, 1 ); +/* + Aig_ManForEachPo( pMan, pObj, i ) + printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vSupps, i) ) ); + printf( "\n" ); +*/ + return vSupps; +} + +/**Function************************************************************* + + Synopsis [Start char-bases support representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Aig_ManSuppCharStart( Vec_Int_t * vOne, int nPis ) +{ + char * pBuffer; + int i, Entry; + pBuffer = ALLOC( char, nPis ); + memset( pBuffer, 0, sizeof(char) * nPis ); + Vec_IntForEachEntry( vOne, Entry, i ) + { + assert( Entry < nPis ); + pBuffer[Entry] = 1; + } + return pBuffer; +} + +/**Function************************************************************* + + Synopsis [Add to char-bases support representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManSuppCharAdd( char * pBuffer, Vec_Int_t * vOne, int nPis ) +{ + int i, Entry; + Vec_IntForEachEntry( vOne, Entry, i ) + { + assert( Entry < nPis ); + pBuffer[Entry] = 1; + } +} + +/**Function************************************************************* + + Synopsis [Find the common variables using char-bases support representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManSuppCharCommon( char * pBuffer, Vec_Int_t * vOne ) +{ + int i, Entry, nCommon = 0; + Vec_IntForEachEntry( vOne, Entry, i ) + nCommon += pBuffer[Entry]; + return nCommon; +} + +/**Function************************************************************* + + Synopsis [Find the best partition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsChar, int nPartSizeLimit, Vec_Int_t * vOne ) +{ + Vec_Int_t * vPartSupp, * vPart; + int Attract, Repulse, Value, ValueBest; + int i, nCommon, iBest; + iBest = -1; + ValueBest = 0; + Vec_PtrForEachEntry( vPartSuppsAll, vPartSupp, i ) + { + vPart = Vec_PtrEntry( vPartsAll, i ); + if ( nPartSizeLimit > 0 && Vec_IntSize(vPart) >= nPartSizeLimit ) + continue; +// nCommon = Vec_IntTwoCountCommon( vPartSupp, vOne ); + nCommon = Aig_ManSuppCharCommon( Vec_PtrEntry(vPartSuppsChar, i), vOne ); + if ( nCommon == 0 ) + continue; + if ( nCommon == Vec_IntSize(vOne) ) + return i; + Attract = 1000 * nCommon / Vec_IntSize(vOne); + if ( Vec_IntSize(vPartSupp) < 100 ) + Repulse = 1; + else + Repulse = 1+Extra_Base2Log(Vec_IntSize(vPartSupp)-100); + Value = Attract/Repulse; + if ( ValueBest < Value ) + { + ValueBest = Value; + iBest = i; + } + } + if ( ValueBest < 75 ) + return -1; + return iBest; +} + +/**Function************************************************************* + + Synopsis [Perform the smart partitioning.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManPartitionPrint( Aig_Man_t * p, Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll ) +{ + Vec_Int_t * vOne; + int i, nOutputs, Counter; + + Counter = 0; + Vec_PtrForEachEntry( vPartSuppsAll, vOne, i ) + { + nOutputs = Vec_IntSize(Vec_PtrEntry(vPartsAll, i)); + printf( "%d=(%d,%d) ", i, Vec_IntSize(vOne), nOutputs ); + Counter += nOutputs; + if ( i == Vec_PtrSize(vPartsAll) - 1 ) + break; + } + assert( Counter == Aig_ManPoNum(p) ); + printf( "\nTotal = %d. Outputs = %d.\n", Counter, Aig_ManPoNum(p) ); +} + +/**Function************************************************************* + + Synopsis [Perform the smart partitioning.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll, int nPartSizeLimit ) +{ + Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp; + int i, iPart; + + if ( nPartSizeLimit == 0 ) + nPartSizeLimit = 200; + + // pack smaller partitions into larger blocks + iPart = 0; + vPart = vPartSupp = NULL; + Vec_PtrForEachEntry( vPartSuppsAll, vOne, i ) + { + if ( Vec_IntSize(vOne) < nPartSizeLimit ) + { + if ( vPartSupp == NULL ) + { + assert( vPart == NULL ); + vPartSupp = Vec_IntDup(vOne); + vPart = Vec_PtrEntry(vPartsAll, i); + } + else + { + vPartSupp = Vec_IntTwoMerge( vTemp = vPartSupp, vOne ); + Vec_IntFree( vTemp ); + vPart = Vec_IntTwoMerge( vTemp = vPart, Vec_PtrEntry(vPartsAll, i) ); + Vec_IntFree( vTemp ); + Vec_IntFree( Vec_PtrEntry(vPartsAll, i) ); + } + if ( Vec_IntSize(vPartSupp) < nPartSizeLimit ) + continue; + } + else + vPart = Vec_PtrEntry(vPartsAll, i); + // add the partition + Vec_PtrWriteEntry( vPartsAll, iPart, vPart ); + vPart = NULL; + if ( vPartSupp ) + { + Vec_IntFree( Vec_PtrEntry(vPartSuppsAll, iPart) ); + Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp ); + vPartSupp = NULL; + } + iPart++; + } + // add the last one + if ( vPart ) + { + Vec_PtrWriteEntry( vPartsAll, iPart, vPart ); + vPart = NULL; + + assert( vPartSupp != NULL ); + Vec_IntFree( Vec_PtrEntry(vPartSuppsAll, iPart) ); + Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp ); + vPartSupp = NULL; + iPart++; + } + Vec_PtrShrink( vPartsAll, iPart ); + Vec_PtrShrink( vPartsAll, iPart ); +} + +/**Function************************************************************* + + Synopsis [Perform the smart partitioning.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Vec_t ** pvPartSupps ) +{ + Vec_Ptr_t * vPartSuppsChar; + Vec_Ptr_t * vSupps, * vPartsAll, * vPartsAll2, * vPartSuppsAll;//, * vPartPtr; + Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp; + int i, iPart, iOut, clk; + + // compute the supports for all outputs +clk = clock(); + vSupps = (Vec_Ptr_t *)Aig_ManSupports( p ); +if ( fVerbose ) +{ +PRT( "Supps", clock() - clk ); +} + // start char-based support representation + vPartSuppsChar = Vec_PtrAlloc( 1000 ); + + // create partitions +clk = clock(); + vPartsAll = Vec_PtrAlloc( 256 ); + vPartSuppsAll = Vec_PtrAlloc( 256 ); + Vec_PtrForEachEntry( vSupps, vOne, i ) + { + // get the output number + iOut = Vec_IntPop(vOne); + // find closely matching part + iPart = Aig_ManPartitionSmartFindPart( vPartSuppsAll, vPartsAll, vPartSuppsChar, nPartSizeLimit, vOne ); +//printf( "%4d->%4d ", i, iPart ); + if ( iPart == -1 ) + { + // create new partition + vPart = Vec_IntAlloc( 32 ); + Vec_IntPush( vPart, iOut ); + // create new partition support + vPartSupp = Vec_IntDup( vOne ); + // add this partition and its support + Vec_PtrPush( vPartsAll, vPart ); + Vec_PtrPush( vPartSuppsAll, vPartSupp ); + + Vec_PtrPush( vPartSuppsChar, Aig_ManSuppCharStart(vOne, Aig_ManPiNum(p)) ); + } + else + { + // add output to this partition + vPart = Vec_PtrEntry( vPartsAll, iPart ); + Vec_IntPush( vPart, iOut ); + // merge supports + vPartSupp = Vec_PtrEntry( vPartSuppsAll, iPart ); + vPartSupp = Vec_IntTwoMerge( vTemp = vPartSupp, vOne ); + Vec_IntFree( vTemp ); + // reinsert new support + Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp ); + + Aig_ManSuppCharAdd( Vec_PtrEntry(vPartSuppsChar, iPart), vOne, Aig_ManPiNum(p) ); + } + } + + // stop char-based support representation + Vec_PtrForEachEntry( vPartSuppsChar, vTemp, i ) + free( vTemp ); + Vec_PtrFree( vPartSuppsChar ); + +//printf( "\n" ); +if ( fVerbose ) +{ +PRT( "Parts", clock() - clk ); +} + +clk = clock(); + // reorder partitions in the decreasing order of support sizes + // remember partition number in each partition support + Vec_PtrForEachEntry( vPartSuppsAll, vOne, i ) + Vec_IntPush( vOne, i ); + // sort the supports in the decreasing order + Vec_VecSort( (Vec_Vec_t *)vPartSuppsAll, 1 ); + // reproduce partitions + vPartsAll2 = Vec_PtrAlloc( 256 ); + Vec_PtrForEachEntry( vPartSuppsAll, vOne, i ) + Vec_PtrPush( vPartsAll2, Vec_PtrEntry(vPartsAll, Vec_IntPop(vOne)) ); + Vec_PtrFree( vPartsAll ); + vPartsAll = vPartsAll2; + + // compact small partitions +// Aig_ManPartitionPrint( p, vPartsAll, vPartSuppsAll ); + Aig_ManPartitionCompact( vPartsAll, vPartSuppsAll, nPartSizeLimit ); + if ( fVerbose ) +// Aig_ManPartitionPrint( p, vPartsAll, vPartSuppsAll ); + printf( "Created %d partitions.\n", Vec_PtrSize(vPartsAll) ); + +if ( fVerbose ) +{ +//PRT( "Comps", clock() - clk ); +} + + // cleanup + Vec_VecFree( (Vec_Vec_t *)vSupps ); + if ( pvPartSupps == NULL ) + Vec_VecFree( (Vec_Vec_t *)vPartSuppsAll ); + else + *pvPartSupps = (Vec_Vec_t *)vPartSuppsAll; +/* + // converts from intergers to nodes + Vec_PtrForEachEntry( vPartsAll, vPart, iPart ) + { + vPartPtr = Vec_PtrAlloc( Vec_IntSize(vPart) ); + Vec_IntForEachEntry( vPart, iOut, i ) + Vec_PtrPush( vPartPtr, Aig_ManPo(p, iOut) ); + Vec_IntFree( vPart ); + Vec_PtrWriteEntry( vPartsAll, iPart, vPartPtr ); + } +*/ + return (Vec_Vec_t *)vPartsAll; +} + +/**Function************************************************************* + + Synopsis [Perform the naive partitioning.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize ) +{ + Vec_Vec_t * vParts; + Aig_Obj_t * pObj; + int nParts, i; + nParts = (Aig_ManPoNum(p) / nPartSize) + ((Aig_ManPoNum(p) % nPartSize) > 0); + vParts = Vec_VecStart( nParts ); + Aig_ManForEachPo( p, pObj, i ) + Vec_VecPush( vParts, i / nPartSize, pObj ); + return vParts; +} + + + +/**Function************************************************************* + + Synopsis [Adds internal nodes in the topological order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Aig_ManDupPart_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + assert( !Aig_IsComplement(pObj) ); + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return pObj->pData; + assert( Aig_ObjIsNode(pObj) ); + Aig_ManDupPart_rec( pNew, p, Aig_ObjFanin0(pObj) ); + Aig_ManDupPart_rec( pNew, p, Aig_ObjFanin1(pObj) ); + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection + Aig_ObjSetTravIdCurrent(p, pObj); + return pObj->pData; +} + +/**Function************************************************************* + + Synopsis [Adds internal nodes in the topological order.] + + Description [Returns the array of new outputs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManDupPart( Aig_Man_t * pNew, Aig_Man_t * p, Vec_Int_t * vPart, Vec_Int_t * vPartSupp, int fInverse ) +{ + Vec_Ptr_t * vOutputs; + Aig_Obj_t * pObj, * pObjNew; + int Entry, k; + // create the PIs + Aig_ManIncrementTravId( p ); + Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + if ( !fInverse ) + { + Vec_IntForEachEntry( vPartSupp, Entry, k ) + { + pObj = Aig_ManPi( p, Entry ); + pObj->pData = Aig_ManPi( pNew, k ); + Aig_ObjSetTravIdCurrent( p, pObj ); + } + } + else + { + Vec_IntForEachEntry( vPartSupp, Entry, k ) + { + pObj = Aig_ManPi( p, k ); + pObj->pData = Aig_ManPi( pNew, Entry ); + Aig_ObjSetTravIdCurrent( p, pObj ); + } + } + // create the internal nodes + vOutputs = Vec_PtrAlloc( Vec_IntSize(vPart) ); + Vec_IntForEachEntry( vPart, Entry, k ) + { + pObj = Aig_ManPo( p, Entry ); + pObjNew = Aig_ManDupPart_rec( pNew, p, Aig_ObjFanin0(pObj) ); + pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) ); + Vec_PtrPush( vOutputs, pObjNew ); + } + return vOutputs; +} + +/**Function************************************************************* + + Synopsis [Create partitioned miter of the two AIGs.] + + Description [Assumes that each output in the second AIG cannot have + more supp vars than the same output in the first AIG.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pMiter; + Vec_Ptr_t * vMiters, * vNodes1, * vNodes2; + Vec_Vec_t * vParts, * vPartSupps; + Vec_Int_t * vPart, * vPartSupp; + int i, k; + // partition the first manager + vParts = Aig_ManPartitionSmart( p1, nPartSize, 0, &vPartSupps ); + // derive miters + vMiters = Vec_PtrAlloc( Vec_VecSize(vParts) ); + for ( i = 0; i < Vec_VecSize(vParts); i++ ) + { + // get partitions and their support + vPart = Vec_PtrEntry( (Vec_Ptr_t *)vParts, i ); + vPartSupp = Vec_PtrEntry( (Vec_Ptr_t *)vPartSupps, i ); + // create the new miter + pNew = Aig_ManStart( 1000 ); + // create the PIs + for ( k = 0; k < Vec_IntSize(vPartSupp); k++ ) + Aig_ObjCreatePi( pNew ); + // copy the components + vNodes1 = Aig_ManDupPart( pNew, p1, vPart, vPartSupp, 0 ); + vNodes2 = Aig_ManDupPart( pNew, p2, vPart, vPartSupp, 0 ); + // create the miter + pMiter = Aig_MiterTwo( pNew, vNodes1, vNodes2 ); + // create the output + Aig_ObjCreatePo( pNew, pMiter ); + // clean up + Aig_ManCleanup( pNew ); + Vec_PtrPush( vMiters, pNew ); + } + Vec_VecFree( vParts ); + Vec_VecFree( vPartSupps ); + return vMiters; +} + +/**Function************************************************************* + + Synopsis [Performs partitioned choice computation.] + + Description [Assumes that each output in the second AIG cannot have + more supp vars than the same output in the first AIG.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize ) +{ + Aig_Man_t * pChoice, * pNew, * pAig, * p; + Aig_Obj_t * pObj; + Vec_Ptr_t * vMiters, * vNodes; + Vec_Vec_t * vParts, * vPartSupps; + Vec_Int_t * vPart, * vPartSupp; + int i, k, m; + + // partition the first AIG + assert( Vec_PtrSize(vAigs) > 1 ); + pAig = Vec_PtrEntry( vAigs, 0 ); + vParts = Aig_ManPartitionSmart( pAig, nPartSize, 0, &vPartSupps ); + + // derive the AIG partitions + vMiters = Vec_PtrAlloc( Vec_VecSize(vParts) ); + for ( i = 0; i < Vec_VecSize(vParts); i++ ) + { + // get partitions and their support + vPart = Vec_PtrEntry( (Vec_Ptr_t *)vParts, i ); + vPartSupp = Vec_PtrEntry( (Vec_Ptr_t *)vPartSupps, i ); + // create the new miter + pNew = Aig_ManStart( 1000 ); + // create the PIs + for ( k = 0; k < Vec_IntSize(vPartSupp); k++ ) + Aig_ObjCreatePi( pNew ); + // copy the components + Vec_PtrForEachEntry( vAigs, p, k ) + { + vNodes = Aig_ManDupPart( pNew, p, vPart, vPartSupp, 0 ); + Vec_PtrForEachEntry( vNodes, pObj, m ) + Aig_ObjCreatePo( pNew, pObj ); + Vec_PtrFree( vNodes ); + } + // add to the partitions + Vec_PtrPush( vMiters, pNew ); + } + + // perform choicing for each derived AIG + Vec_PtrForEachEntry( vMiters, pNew, i ) + { + extern Aig_Man_t * Fra_Choice( Aig_Man_t * pManAig ); + pNew = Fra_Choice( p = pNew ); + Vec_PtrWriteEntry( vMiters, i, pNew ); + Aig_ManStop( p ); + } + + // combine the resulting AIGs + pNew = Aig_ManStartFrom( pAig ); + Vec_PtrForEachEntry( vMiters, p, i ) + { + // get partitions and their support + vPart = Vec_PtrEntry( (Vec_Ptr_t *)vParts, i ); + vPartSupp = Vec_PtrEntry( (Vec_Ptr_t *)vPartSupps, i ); + // copy the component + vNodes = Aig_ManDupPart( pNew, p, vPart, vPartSupp, 1 ); + assert( Vec_PtrSize(vNodes) == Vec_VecSize(vParts) * Vec_PtrSize(vAigs) ); + // create choice node + for ( k = 0; k < Vec_VecSize(vParts); k++ ) + { + for ( m = 0; m < Vec_PtrSize(vAigs); m++ ) + { + pObj = Aig_ObjChild0( Vec_PtrEntry(vNodes, k * Vec_PtrSize(vAigs) + m) ); + break; + } + Aig_ObjCreatePo( pNew, pObj ); + } + Vec_PtrFree( vNodes ); + } + Vec_VecFree( vParts ); + Vec_VecFree( vPartSupps ); + + // trasfer representatives + Aig_ManReprStart( pNew, Aig_ManObjIdMax(pNew)+1 ); + Vec_PtrForEachEntry( vMiters, p, i ) + { + Aig_ManTransferRepr( pNew, p ); + Aig_ManStop( p ); + } + Vec_PtrFree( vMiters ); + + // derive the result of choicing + pChoice = Aig_ManCreateChoices( pNew ); + if ( pChoice != pNew ) + Aig_ManStop( pNew ); + return pChoice; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c new file mode 100644 index 00000000..fa6bf60e --- /dev/null +++ b/src/aig/aig/aigRepr.c @@ -0,0 +1,343 @@ +/**CFile**************************************************************** + + FileName [aigRepr.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Handing node representatives.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigRepr.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the array of representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManReprStart( Aig_Man_t * p, int nIdMax ) +{ + assert( Aig_ManBufNum(p) == 0 ); + assert( p->pRepr == NULL ); + p->nReprAlloc = nIdMax; + p->pRepr = ALLOC( Aig_Obj_t *, p->nReprAlloc ); + memset( p->pRepr, 0, sizeof(Aig_Obj_t *) * p->nReprAlloc ); +} + +/**Function************************************************************* + + Synopsis [Stop the array of representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManReprStop( Aig_Man_t * p ) +{ + assert( p->pRepr != NULL ); + FREE( p->pRepr ); + p->nReprAlloc = 0; +} + +/**Function************************************************************* + + Synopsis [Set the representative.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 ) +{ + assert( p->pRepr != NULL ); + assert( !Aig_IsComplement(pNode1) ); + assert( !Aig_IsComplement(pNode2) ); + assert( pNode1->Id < p->nReprAlloc ); + assert( pNode2->Id < p->nReprAlloc ); + if ( pNode1 == pNode2 ) + return; + if ( pNode1->Id < pNode2->Id ) + p->pRepr[pNode2->Id] = pNode1; + else + p->pRepr[pNode1->Id] = pNode2; +} + +/**Function************************************************************* + + Synopsis [Find representative.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Aig_Obj_t * Aig_ObjFindRepr( Aig_Man_t * p, Aig_Obj_t * pNode ) +{ + assert( p->pRepr != NULL ); + assert( !Aig_IsComplement(pNode) ); + assert( pNode->Id < p->nReprAlloc ); + assert( !p->pRepr[pNode->Id] || p->pRepr[pNode->Id]->Id < pNode->Id ); + return p->pRepr[pNode->Id]; +} + +/**Function************************************************************* + + Synopsis [Find representative transitively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Aig_Obj_t * Aig_ObjFindReprTrans( Aig_Man_t * p, Aig_Obj_t * pNode ) +{ + Aig_Obj_t * pPrev, * pRepr; + for ( pPrev = NULL, pRepr = Aig_ObjFindRepr(p, pNode); pRepr; pPrev = pRepr, pRepr = Aig_ObjFindRepr(p, pRepr) ); + return pPrev; +} + +/**Function************************************************************* + + Synopsis [Returns representatives of fanin in approapriate polarity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Aig_Obj_t * Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pRepr; + if ( pRepr = Aig_ObjFindRepr(p, pObj) ) + return Aig_NotCond( pRepr->pData, pObj->fPhase ^ pRepr->fPhase ); + return pObj->pData; +} +static inline Aig_Obj_t * Aig_ObjChild0Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjRepr(p, Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) ); } +static inline Aig_Obj_t * Aig_ObjChild1Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjRepr(p, Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) ); } + +/**Function************************************************************* + + Synopsis [Duplicates AIG while substituting representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p ) +{ + Aig_Obj_t * pObj, * pRepr; + int k; + assert( pNew->pRepr != NULL ); + // go through the nodes which have representatives + Aig_ManForEachObj( p, pObj, k ) + if ( pRepr = Aig_ObjFindRepr(p, pObj) ) + Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) ); +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG while substituting representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pRepr; + int i; + // start the HOP package + pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); + Aig_ManReprStart( pNew, Aig_ManObjIdMax(p)+1 ); + // map the const and primary inputs + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePi(pNew); + // map the internal nodes + Aig_ManForEachNode( p, pObj, i ) + { + pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) ); + if ( pRepr = Aig_ObjFindRepr(p, pObj) ) // member of the class + Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) ); + } + // transfer the POs + Aig_ManForEachPo( p, pObj, i ) + Aig_ObjCreatePo( pNew, Aig_ObjChild0Repr(p, pObj) ); + // check the new manager + if ( !Aig_ManCheck(pNew) ) + printf( "Aig_ManDupRepr: Check has failed.\n" ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Transfer representatives and return the number of critical fanouts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManRemapRepr( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj, * pRepr; + int i, nFanouts = 0; + Aig_ManForEachNode( p, pObj, i ) + { + pRepr = Aig_ObjFindReprTrans( p, pObj ); + if ( pRepr == NULL ) + continue; + assert( pRepr->Id < pObj->Id ); + Aig_ObjSetRepr( p, pObj, pRepr ); + nFanouts += (pObj->nRefs > 0); + } + return nFanouts; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pNode, Aig_Obj_t * pOld ) +{ + // check the trivial cases + if ( pNode == NULL ) + return 0; +// if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode +// return 0; + if ( pNode == pOld ) + return 1; + // skip the visited node + if ( Aig_ObjIsTravIdCurrent( p, pNode ) ) + return 0; + Aig_ObjSetTravIdCurrent( p, pNode ); + // check the children + if ( Aig_ObjCheckTfi_rec( p, Aig_ObjFanin0(pNode), pOld ) ) + return 1; + if ( Aig_ObjCheckTfi_rec( p, Aig_ObjFanin1(pNode), pOld ) ) + return 1; + // check equivalent nodes + return Aig_ObjCheckTfi_rec( p, pNode->pData, pOld ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld ) +{ + assert( !Aig_IsComplement(pNew) ); + assert( !Aig_IsComplement(pOld) ); + Aig_ManIncrementTravId( p ); + return Aig_ObjCheckTfi_rec( p, pNew, pOld ); +} + +/**Function************************************************************* + + Synopsis [Creates choices.] + + Description [The input AIG is assumed to have representatives assigned.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManCreateChoices( Aig_Man_t * p ) +{ + Aig_Man_t * pTemp; + Aig_Obj_t * pObj, * pRepr; + int i; + assert( p->pRepr != NULL ); + // iteratively reconstruct the HOP manager while transfering the fanouts + while ( Aig_ManRemapRepr( p ) ) + { + p = Aig_ManDupRepr( pTemp = p ); + Aig_ManStop( pTemp ); + } + // create choices in this manager + Aig_ManCleanData( p ); + // make the choice nodes + Aig_ManForEachNode( p, pObj, i ) + { + pRepr = Aig_ObjFindRepr( p, pObj ); + if ( pRepr == NULL ) + continue; + // skip constant and PI classes + if ( !Aig_ObjIsNode(pRepr) ) + continue; + // skip choices with combinatinal loops + if ( Aig_ObjCheckTfi( p, pRepr, pObj ) ) + continue; + // add choice to the choice node + pObj->pData = pRepr->pData; + pRepr->pData = pObj; + } + return p; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c index ba359c09..0d4ffd1f 100644 --- a/src/aig/aig/aigTable.c +++ b/src/aig/aig/aigTable.c @@ -99,7 +99,7 @@ clk = clock(); } nEntries = Aig_ManNodeNum(p); assert( Counter == nEntries ); - printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize ); +// printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize ); PRT( "Time", clock() - clk ); // replace the table and the parameters free( pTableOld ); diff --git a/src/aig/aig/aigTiming.c b/src/aig/aig/aigTiming.c index dfb4c306..14ee4f2c 100644 --- a/src/aig/aig/aigTiming.c +++ b/src/aig/aig/aigTiming.c @@ -68,6 +68,22 @@ static inline void Aig_ObjSetReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj, int /**Function************************************************************* + Synopsis [Resets reverse level of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ObjClearReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + Aig_ObjSetReverseLevel( p, pObj, 0 ); +} + +/**Function************************************************************* + Synopsis [Returns required level of the node.] Description [Converts the reverse levels of the node into its required @@ -178,6 +194,7 @@ void Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew ) Aig_Obj_t * pFanout, * pTemp; int iFanout, LevelOld, Lev, k, m; assert( p->pFanData != NULL ); + assert( Aig_ObjIsNode(pObjNew) ); // allocate level if needed if ( p->vLevels == NULL ) p->vLevels = Vec_VecAlloc( Aig_ManLevels(p) + 8 ); @@ -203,8 +220,9 @@ void Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew ) // schedule fanout for level update Aig_ObjForEachFanout( p, pTemp, pFanout, iFanout, m ) { - if ( !Aig_ObjIsPo(pFanout) && !pFanout->fMarkA ) + if ( Aig_ObjIsNode(pFanout) && !pFanout->fMarkA ) { + assert( Aig_ObjLevel(pFanout) >= Lev ); Vec_VecPush( p->vLevels, Aig_ObjLevel(pFanout), pFanout ); pFanout->fMarkA = 1; } @@ -226,8 +244,9 @@ void Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew ) void Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew ) { Aig_Obj_t * pFanin, * pTemp; - int LevelOld, Lev, k; + int LevelOld, LevFanin, Lev, k; assert( p->vLevelR != NULL ); + assert( Aig_ObjIsNode(pObjNew) ); // allocate level if needed if ( p->vLevels == NULL ) p->vLevels = Vec_VecAlloc( Aig_ManLevels(p) + 8 ); @@ -253,20 +272,77 @@ void Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew ) continue; // schedule fanins for level update pFanin = Aig_ObjFanin0(pTemp); - if ( pFanin && !Aig_ObjIsPi(pFanin) && !pFanin->fMarkA ) + if ( Aig_ObjIsNode(pFanin) && !pFanin->fMarkA ) { - Vec_VecPush( p->vLevels, Aig_ObjReverseLevel(p, pFanin), pFanin ); + LevFanin = Aig_ObjReverseLevel( p, pFanin ); + assert( LevFanin >= Lev ); + Vec_VecPush( p->vLevels, LevFanin, pFanin ); pFanin->fMarkA = 1; } pFanin = Aig_ObjFanin1(pTemp); - if ( pFanin && !Aig_ObjIsPi(pFanin) && !pFanin->fMarkA ) + if ( Aig_ObjIsNode(pFanin) && !pFanin->fMarkA ) { - Vec_VecPush( p->vLevels, Aig_ObjReverseLevel(p, pFanin), pFanin ); + LevFanin = Aig_ObjReverseLevel( p, pFanin ); + assert( LevFanin >= Lev ); + Vec_VecPush( p->vLevels, LevFanin, pFanin ); pFanin->fMarkA = 1; } } } +/**Function************************************************************* + + Synopsis [Verifies direct level of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManVerifyLevel( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0; + assert( p->pFanData ); + Aig_ManForEachNode( p, pObj, i ) + if ( Aig_ObjLevel(pObj) != Aig_ObjLevelNew(pObj) ) + { + printf( "Level of node %6d should be %4d instead of %4d.\n", + pObj->Id, Aig_ObjLevelNew(pObj), Aig_ObjLevel(pObj) ); + Counter++; + } + if ( Counter ) + printf( "Levels of %d nodes are incorrect.\n", Counter ); +} + +/**Function************************************************************* + + Synopsis [Verifies reverse level of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManVerifyReverseLevel( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0; + assert( p->vLevelR ); + Aig_ManForEachNode( p, pObj, i ) + if ( Aig_ObjLevel(pObj) != Aig_ObjLevelNew(pObj) ) + { + printf( "Reverse level of node %6d should be %4d instead of %4d.\n", + pObj->Id, Aig_ObjReverseLevelNew(p, pObj), Aig_ObjReverseLevel(p, pObj) ); + Counter++; + } + if ( Counter ) + printf( "Reverse levels of %d nodes are incorrect.\n", Counter ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index a1c68371..364c32a3 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -123,6 +123,44 @@ void Aig_ManCheckMarkA( Aig_Man_t * p ) /**Function************************************************************* + Synopsis [Checks if the markA is reset.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManCleanMarkA( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManForEachObj( p, pObj, i ) + pObj->fMarkA = 0; +} + +/**Function************************************************************* + + Synopsis [Checks if the markA is reset.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManCleanMarkB( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManForEachObj( p, pObj, i ) + pObj->fMarkB = 0; +} + +/**Function************************************************************* + Synopsis [Cleans the data pointers for the nodes.] Description [] diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make index 83e4c413..d4737278 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/aigMffc.c \ src/aig/aig/aigObj.c \ src/aig/aig/aigOper.c \ + src/aig/aig/aigOrder.c \ + src/aig/aig/aigPart.c \ + src/aig/aig/aigRepr.c \ src/aig/aig/aigSeq.c \ src/aig/aig/aigTable.c \ src/aig/aig/aigTiming.c \ diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index c758867c..2f121752 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -83,8 +83,16 @@ struct Cnf_Man_t_ int nMergeLimit; // the limit on the size of merged cut unsigned * pTruths[4]; // temporary truth tables Vec_Int_t * vMemory; // memory for intermediate ISOP representation + int timeCuts; + int timeMap; + int timeSave; }; + +static inline Dar_Cut_t * Dar_ObjBestCut( Aig_Obj_t * pObj ) { Dar_Cut_t * pCut; int i; Dar_ObjForEachCut( pObj, pCut, i ) if ( pCut->fBest ) return pCut; return NULL; } + +static inline int Cnf_CutSopCost( Cnf_Man_t * p, Dar_Cut_t * pCut ) { return p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth]; } + static inline int Cnf_CutLeaveNum( Cnf_Cut_t * pCut ) { return pCut->nFanins; } static inline int * Cnf_CutLeaves( Cnf_Cut_t * pCut ) { return pCut->pFanins; } static inline unsigned * Cnf_CutTruth( Cnf_Cut_t * pCut ) { return (unsigned *)(pCut->pFanins + pCut->nFanins); } @@ -109,7 +117,9 @@ static inline void Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut //////////////////////////////////////////////////////////////////////// /*=== cnfCore.c ========================================================*/ -extern Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Aig_Man_t * pAig ); +extern Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig ); +extern Cnf_Man_t * Cnf_ManRead(); +extern void Cnf_ClearMemory(); /*=== cnfCut.c ========================================================*/ extern Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj ); extern void Cnf_CutPrint( Cnf_Cut_t * pCut ); @@ -121,10 +131,12 @@ extern void Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops ); /*=== cnfMan.c ========================================================*/ extern Cnf_Man_t * Cnf_ManStart(); extern void Cnf_ManStop( Cnf_Man_t * p ); +extern Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ); extern void Cnf_DataFree( Cnf_Dat_t * p ); extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName ); void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p ); /*=== cnfMap.c ========================================================*/ +extern void Cnf_DeriveMapping( Cnf_Man_t * p ); extern int Cnf_ManMapForCnf( Cnf_Man_t * p ); /*=== cnfPost.c ========================================================*/ extern void Cnf_ManTransferCuts( Cnf_Man_t * p ); @@ -132,7 +144,7 @@ extern void Cnf_ManFreeCuts( Cnf_Man_t * p ); extern void Cnf_ManPostprocess( Cnf_Man_t * p ); /*=== cnfUtil.c ========================================================*/ extern Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect ); -extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect ); +extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder ); /*=== cnfWrite.c ========================================================*/ extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover ); extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped ); diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c index a3a7efaa..7480d45d 100644 --- a/src/aig/cnf/cnfCore.c +++ b/src/aig/cnf/cnfCore.c @@ -24,13 +24,15 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static Cnf_Man_t * s_pManCnf = NULL; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [] + Synopsis [Converts AIG into the SAT solver.] Description [] @@ -39,21 +41,97 @@ SeeAlso [] ***********************************************************************/ -Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Aig_Man_t * pAig ) +Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig ) { - Aig_MmFixed_t * pMemCuts; - Cnf_Dat_t * pCnf = NULL; + Cnf_Man_t * p; + Cnf_Dat_t * pCnf; Vec_Ptr_t * vMapped; - int nIters = 2; + Aig_MmFixed_t * pMemCuts; int clk; - + // allocate the CNF manager + if ( s_pManCnf == NULL ) + s_pManCnf = Cnf_ManStart(); // connect the managers + p = s_pManCnf; p->pManAig = pAig; // generate cuts for all nodes, assign cost, and find best cuts clk = clock(); - pMemCuts = Dar_ManComputeCuts( pAig ); -PRT( "Cuts", clock() - clk ); + pMemCuts = Dar_ManComputeCuts( pAig, 10 ); +p->timeCuts = clock() - clk; + + // find the mapping +clk = clock(); + Cnf_DeriveMapping( p ); +p->timeMap = clock() - clk; +// Aig_ManScanMapping( p, 1 ); + + // convert it into CNF +clk = clock(); + Cnf_ManTransferCuts( p ); + vMapped = Cnf_ManScanMapping( p, 1, 1 ); + pCnf = Cnf_ManWriteCnf( p, vMapped ); + Vec_PtrFree( vMapped ); + Aig_MmFixedStop( pMemCuts, 0 ); +p->timeSave = clock() - clk; + +PRT( "Cuts ", p->timeCuts ); +PRT( "Map ", p->timeMap ); +PRT( "Saving ", p->timeSave ); + return pCnf; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cnf_Man_t * Cnf_ManRead() +{ + return s_pManCnf; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cnf_ClearMemory() +{ + if ( s_pManCnf == NULL ) + return; + Cnf_ManStop( s_pManCnf ); + s_pManCnf = NULL; +} + + +#if 0 + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cnf_Dat_t * Cnf_Derive_old( Aig_Man_t * pAig ) +{ /* // iteratively improve area flow for ( i = 0; i < nIters; i++ ) @@ -95,6 +173,9 @@ PRT( "Ext ", clock() - clk ); return NULL; } +#endif + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/cnf/cnfCut.c b/src/aig/cnf/cnfCut.c index afe5920a..17ab0c78 100644 --- a/src/aig/cnf/cnfCut.c +++ b/src/aig/cnf/cnfCut.c @@ -87,15 +87,14 @@ Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj ) Cnf_Cut_t * pCut; unsigned * pTruth; assert( Aig_ObjIsNode(pObj) ); -// pCutBest = Aig_ObjBestCut( pObj ); - pCutBest = NULL; + pCutBest = Dar_ObjBestCut( pObj ); assert( pCutBest != NULL ); assert( pCutBest->nLeaves <= 4 ); pCut = Cnf_CutAlloc( p, pCutBest->nLeaves ); memcpy( pCut->pFanins, pCutBest->pLeaves, sizeof(int) * pCutBest->nLeaves ); pTruth = Cnf_CutTruth(pCut); *pTruth = (pCutBest->uTruth << 16) | pCutBest->uTruth; - pCut->Cost = p->pSopSizes[0xFFFF & *pTruth] + p->pSopSizes[0xFFFF & ~*pTruth]; + pCut->Cost = Cnf_CutSopCost( p, pCutBest ); return pCut; } diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index e978e322..77bf8650 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -86,6 +86,28 @@ void Cnf_ManStop( Cnf_Man_t * p ) /**Function************************************************************* + Synopsis [Returns the array of CI IDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) +{ + Vec_Int_t * vCiIds; + Aig_Obj_t * pObj; + int i; + vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) ); + Aig_ManForEachPi( p, pObj, i ) + Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] ); + return vCiIds; +} + +/**Function************************************************************* + Synopsis [] Description [] diff --git a/src/aig/cnf/cnfMap.c b/src/aig/cnf/cnfMap.c index a9ba41a0..ad728412 100644 --- a/src/aig/cnf/cnfMap.c +++ b/src/aig/cnf/cnfMap.c @@ -28,6 +28,126 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Computes area flow of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut, int * pAreaFlows ) +{ + Aig_Obj_t * pLeaf; + int i; + pCut->Value = 0; + pCut->uSign = 100 * Cnf_CutSopCost( p, pCut ); + Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i ) + { + pCut->Value += pLeaf->nRefs; + if ( !Aig_ObjIsNode(pLeaf) ) + continue; + assert( pLeaf->nRefs > 0 ); + pCut->uSign += pAreaFlows[pLeaf->Id] / (pLeaf->nRefs? pLeaf->nRefs : 1); + } +} + +/**Function************************************************************* + + Synopsis [Computes area flow of the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cnf_CutSuperAreaFlow( Vec_Ptr_t * vSuper, int * pAreaFlows ) +{ + Aig_Obj_t * pLeaf; + int i, nAreaFlow; + nAreaFlow = 100 * (Vec_PtrSize(vSuper) + 1); + Vec_PtrForEachEntry( vSuper, pLeaf, i ) + { + pLeaf = Aig_Regular(pLeaf); + if ( !Aig_ObjIsNode(pLeaf) ) + continue; + assert( pLeaf->nRefs > 0 ); + nAreaFlow += pAreaFlows[pLeaf->Id] / (pLeaf->nRefs? pLeaf->nRefs : 1); + } + return nAreaFlow; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cnf_DeriveMapping( Cnf_Man_t * p ) +{ + Vec_Ptr_t * vSuper; + Aig_Obj_t * pObj; + Dar_Cut_t * pCut, * pCutBest; + int i, k, AreaFlow, * pAreaFlows; + // allocate area flows + pAreaFlows = ALLOC( int, Aig_ManObjIdMax(p->pManAig) + 1 ); + memset( pAreaFlows, 0, sizeof(int) * (Aig_ManObjIdMax(p->pManAig) + 1) ); + // visit the nodes in the topological order and update their best cuts + vSuper = Vec_PtrAlloc( 100 ); + Aig_ManForEachNode( p->pManAig, pObj, i ) + { + // go through the cuts + pCutBest = NULL; + Dar_ObjForEachCut( pObj, pCut, k ) + { + pCut->fBest = 0; + if ( k == 0 ) + continue; + Cnf_CutAssignAreaFlow( p, pCut, pAreaFlows ); + if ( pCutBest == NULL || pCutBest->uSign > pCut->uSign || + (pCutBest->uSign == pCut->uSign && pCutBest->Value < pCut->Value) ) + pCutBest = pCut; + } + // check the big cut +// Aig_ObjCollectSuper( pObj, vSuper ); + // get the area flow of this cut +// AreaFlow = Cnf_CutSuperAreaFlow( vSuper, pAreaFlows ); + AreaFlow = AIG_INFINITY; + if ( AreaFlow >= (int)pCutBest->uSign ) + { + pAreaFlows[pObj->Id] = pCutBest->uSign; + pCutBest->fBest = 1; + } + else + { + pAreaFlows[pObj->Id] = AreaFlow; + pObj->fMarkB = 1; // mark the special node + } + } + Vec_PtrFree( vSuper ); + free( pAreaFlows ); + +/* + // compute the area of mapping + AreaFlow = 0; + Aig_ManForEachPo( p->pManAig, pObj, i ) + AreaFlow += Dar_ObjBestCut(Aig_ObjFanin0(pObj))->uSign / 100 / Aig_ObjFanin0(pObj)->nRefs; + printf( "Area of the network = %d.\n", AreaFlow ); +*/ +} + + + #if 0 /**Function************************************************************* @@ -160,45 +280,6 @@ Dar_Cut_t * Cnf_ObjFindBestCut( Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut ) -{ - Aig_Obj_t * pLeaf; - int i; - pCut->Cost = p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth]; - pCut->Area = (float)pCut->Cost; - pCut->NoRefs = 0; - pCut->FanRefs = 0; - Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i ) - { - if ( !Aig_ObjIsNode(pLeaf) ) - continue; - if ( pLeaf->nRefs == 0 ) - { - pCut->Area += Aig_ObjBestCut(pLeaf)->Area; - pCut->NoRefs++; - } - else - { - pCut->Area += Aig_ObjBestCut(pLeaf)->Area / pLeaf->nRefs; - if ( pCut->FanRefs + pLeaf->nRefs > 15 ) - pCut->FanRefs = 15; - else - pCut->FanRefs += pLeaf->nRefs; - } - } -} - -/**Function************************************************************* - - Synopsis [Computes area flow of the cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ void Cnf_CutAssignArea( Cnf_Man_t * p, Dar_Cut_t * pCut ) { Aig_Obj_t * pLeaf; diff --git a/src/aig/cnf/cnfUtil.c b/src/aig/cnf/cnfUtil.c index da5edef2..22b30262 100644 --- a/src/aig/cnf/cnfUtil.c +++ b/src/aig/cnf/cnfUtil.c @@ -51,11 +51,24 @@ int Aig_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped if ( vMapped ) Vec_PtrPush( vMapped, pObj ); // visit the transitive fanin of the selected cut -// pCutBest = Aig_ObjBestCut(pObj); - pCutBest = NULL; - aArea = pCutBest->Value; - Dar_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i ) - aArea += Aig_ManScanMapping_rec( p, pLeaf, vMapped ); + if ( pObj->fMarkB ) + { + Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 ); + Aig_ObjCollectSuper( pObj, vSuper ); + aArea = Vec_PtrSize(vSuper) + 1; + Vec_PtrForEachEntry( vSuper, pLeaf, i ) + aArea += Aig_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped ); + Vec_PtrFree( vSuper ); + //////////////////////////// + pObj->fMarkB = 1; + } + else + { + pCutBest = Dar_ObjBestCut( pObj ); + aArea = Cnf_CutSopCost( p, pCutBest ); + Dar_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i ) + aArea += Aig_ManScanMapping_rec( p, pLeaf, vMapped ); + } return aArea; } @@ -85,7 +98,7 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect ) p->aArea = 0; Aig_ManForEachPo( p->pManAig, pObj, i ) p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped ); - printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea ); + printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 ); return vMapped; } @@ -100,7 +113,7 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect ) SeeAlso [] ***********************************************************************/ -int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped ) +int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped, int fPreorder ) { Aig_Obj_t * pLeaf; Cnf_Cut_t * pCutBest; @@ -109,15 +122,32 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped return 0; assert( Aig_ObjIsAnd(pObj) ); assert( pObj->pData != NULL ); + // add the node to the mapping + if ( vMapped && fPreorder ) + Vec_PtrPush( vMapped, pObj ); // visit the transitive fanin of the selected cut - pCutBest = pObj->pData; - assert( pCutBest->Cost < 127 ); - aArea = pCutBest->Cost; - Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i ) - aArea += Cnf_ManScanMapping_rec( p, pLeaf, vMapped ); - // collect the node first to derive pre-order - if ( vMapped ) - Vec_PtrPush( vMapped, pObj ); + if ( pObj->fMarkB ) + { + Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 ); + Aig_ObjCollectSuper( pObj, vSuper ); + aArea = Vec_PtrSize(vSuper) + 1; + Vec_PtrForEachEntry( vSuper, pLeaf, i ) + aArea += Cnf_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped, fPreorder ); + Vec_PtrFree( vSuper ); + //////////////////////////// + pObj->fMarkB = 1; + } + else + { + pCutBest = pObj->pData; + assert( pCutBest->Cost < 127 ); + aArea = pCutBest->Cost; + Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i ) + aArea += Cnf_ManScanMapping_rec( p, pLeaf, vMapped, fPreorder ); + } + // add the node to the mapping + if ( vMapped && !fPreorder ) + Vec_PtrPush( vMapped, pObj ); return aArea; } @@ -132,7 +162,7 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect ) +Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder ) { Vec_Ptr_t * vMapped = NULL; Aig_Obj_t * pObj; @@ -146,8 +176,8 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect ) // collect nodes reachable from POs in the DFS order through the best cuts p->aArea = 0; Aig_ManForEachPo( p->pManAig, pObj, i ) - p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped ); - printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea ); + p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped, fPreorder ); + printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 ); return vMapped; } diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c index 22c4240a..41a00732 100644 --- a/src/aig/cnf/cnfWrite.c +++ b/src/aig/cnf/cnfWrite.c @@ -127,42 +127,15 @@ int Cnf_IsopCountLiterals( Vec_Int_t * vIsop, int nVars ) SeeAlso [] ***********************************************************************/ -int Cnf_SopWriteCube( char Cube, int * pVars, int fCompl, int * pLiterals ) -{ - int nLits = 4, b; - for ( b = 0; b < 4; b++ ) - { - if ( Cube % 3 == 0 ) - *pLiterals++ = 2 * pVars[b] + !fCompl; - else if ( Cube % 3 == 1 ) - *pLiterals++ = 2 * pVars[b] + fCompl; - else - nLits--; - Cube = Cube / 3; - } - return nLits; -} - -/**Function************************************************************* - - Synopsis [Writes the cube and returns the number of literals in it.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int fCompl, int * pLiterals ) +int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int * pLiterals ) { int nLits = nVars, b; for ( b = 0; b < nVars; b++ ) { - if ( (Cube & 3) == 1 ) - *pLiterals++ = 2 * pVars[b] + !fCompl; - else if ( (Cube & 3) == 2 ) - *pLiterals++ = 2 * pVars[b] + fCompl; + if ( (Cube & 3) == 1 ) // value 0 --> write positive literal + *pLiterals++ = 2 * pVars[b]; + else if ( (Cube & 3) == 2 ) // value 1 --> write negative literal + *pLiterals++ = 2 * pVars[b] + 1; else nLits--; Cube >>= 2; @@ -186,9 +159,10 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped ) Aig_Obj_t * pObj; Cnf_Dat_t * pCnf; Cnf_Cut_t * pCut; + Vec_Int_t * vCover, * vSopTemp; int OutVar, pVars[32], * pLits, ** pClas; unsigned uTruth; - int i, k, nLiterals, nClauses, nCubes, Cube, Number; + int i, k, nLiterals, nClauses, Cube, Number; // count the number of literals and clauses nLiterals = 1 + Aig_ManPoNum( p->pManAig ); @@ -249,6 +223,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped ) pCnf->nVars = Number; // assign the clauses + vSopTemp = Vec_IntAlloc( 1 << 16 ); pLits = pCnf->pClauses[0]; pClas = pCnf->pClauses; Vec_PtrForEachEntry( vMapped, pObj, i ) @@ -267,48 +242,36 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped ) if ( pCut->nFanins < 5 ) { uTruth = 0xFFFF & *Cnf_CutTruth(pCut); - nCubes = p->pSopSizes[uTruth]; - for ( k = 0; k < nCubes; k++ ) - { - *pClas++ = pLits; - *pLits++ = 2 * OutVar + 1; - pLits += Cnf_SopWriteCube( p->pSops[uTruth][k], pVars, 0, pLits ); - } + Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp ); + vCover = vSopTemp; } else + vCover = pCut->vIsop[1]; + Vec_IntForEachEntry( vCover, Cube, k ) { - Vec_IntForEachEntry( pCut->vIsop[1], Cube, k ) - { - *pClas++ = pLits; - *pLits++ = 2 * OutVar + 1; - pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, 0, pLits ); - } + *pClas++ = pLits; + *pLits++ = 2 * OutVar; + pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits ); } // negative polarity of the cut if ( pCut->nFanins < 5 ) { uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut); - nCubes = p->pSopSizes[uTruth]; - for ( k = 0; k < nCubes; k++ ) - { - *pClas++ = pLits; - *pLits++ = 2 * OutVar; - pLits += Cnf_SopWriteCube( p->pSops[uTruth][k], pVars, 1, pLits ); - } + Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp ); + vCover = vSopTemp; } else + vCover = pCut->vIsop[0]; + Vec_IntForEachEntry( vCover, Cube, k ) { - Vec_IntForEachEntry( pCut->vIsop[0], Cube, k ) - { - *pClas++ = pLits; - *pLits++ = 2 * OutVar; - pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, 1, pLits ); - } + *pClas++ = pLits; + *pLits++ = 2 * OutVar + 1; + pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits ); } -//printf( "%d ", pClas-pCnf->pClauses ); } - + Vec_IntFree( vSopTemp ); + // write the constant literal OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ]; assert( OutVar <= Aig_ManObjIdMax(p->pManAig) ); diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h index 3106c7ad..44dd2788 100644 --- a/src/aig/dar/dar.h +++ b/src/aig/dar/dar.h @@ -44,6 +44,7 @@ struct Dar_RwrPar_t_ { int nCutsMax; // the maximum number of cuts to try int nSubgMax; // the maximum number of subgraphs to try + int fFanout; // support fanout representation int fUpdateLevel; // update level int fUseZeros; // performs zero-cost replacement int fVerbose; // enables verbose output @@ -79,12 +80,13 @@ extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ); /*=== darCore.c ========================================================*/ 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 ); +extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax ); /*=== 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 ); +extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ); +extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ); #ifdef __cplusplus } diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c index 969e5253..097f1a4d 100644 --- a/src/aig/dar/darBalance.c +++ b/src/aig/dar/darBalance.c @@ -53,7 +53,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) Vec_Vec_t * vStore; int i; // create the new manager - pNew = Aig_ManStart(); + pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); // map the PI nodes Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c index 7546df0b..b74f570c 100644 --- a/src/aig/dar/darCore.c +++ b/src/aig/dar/darCore.c @@ -44,6 +44,7 @@ void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars ) memset( pPars, 0, sizeof(Dar_RwrPar_t) ); pPars->nCutsMax = 8; pPars->nSubgMax = 5; // 5 is a "magic number" + pPars->fFanout = 1; pPars->fUpdateLevel = 0; pPars->fUseZeros = 0; pPars->fVerbose = 0; @@ -76,7 +77,8 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars ) // remove dangling nodes Aig_ManCleanup( pAig ); // if updating levels is requested, start fanout and timing - Aig_ManCreateFanout( pAig ); + if ( p->pPars->fFanout ) + Aig_ManFanoutStart( pAig ); if ( p->pPars->fUpdateLevel ) Aig_ManStartReverseLevels( pAig, 0 ); // set elementary cuts for the PIs @@ -85,19 +87,27 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars ) clkStart = clock(); p->nNodesInit = Aig_ManNodeNum(pAig); nNodesOld = Vec_PtrSize( pAig->vObjs ); + pProgress = Extra_ProgressBarStart( stdout, nNodesOld ); Aig_ManForEachObj( pAig, pObj, i ) +// pProgress = Extra_ProgressBarStart( stdout, 100 ); +// Aig_ManOrderStart( pAig ); +// Aig_ManForEachNodeInOrder( pAig, pObj ) { +// Extra_ProgressBarUpdate( pProgress, 100*pAig->nAndPrev/pAig->nAndTotal, NULL ); + Extra_ProgressBarUpdate( pProgress, i, NULL ); if ( !Aig_ObjIsNode(pObj) ) continue; if ( i > nNodesOld ) break; + // consider freeing the cuts // if ( (i & 0xFFF) == 0 && Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) > 100 ) // Dar_ManCutsStart( p ); // compute cuts for the node + p->nNodesTried++; clk = clock(); Dar_ObjComputeCuts_rec( p, pObj ); p->timeCuts += clock() - clk; @@ -133,7 +143,10 @@ p->timeCuts += clock() - clk; Dar_LibEval( p, pObj, pCut, Required ); // check the best gain if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) ) + { +// Aig_ObjOrderAdvance( pAig ); continue; + } // remove the old cuts Dar_ObjSetCuts( pObj, NULL ); // if we end up here, a rewriting step is accepted @@ -149,6 +162,8 @@ p->timeCuts += clock() - clk; // count gains of this class p->ClassGains[p->ClassBest] += nNodeBefore - nNodeAfter; } +// Aig_ManOrderStop( pAig ); + p->timeTotal = clock() - clkStart; p->timeOther = p->timeTotal - p->timeCuts - p->timeEval; @@ -158,9 +173,14 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval; // put the nodes into the DFS order and reassign their IDs // Aig_NtkReassignIds( p ); // fix the levels - Aig_ManDeleteFanout( pAig ); +// Aig_ManVerifyLevel( pAig ); + if ( p->pPars->fFanout ) + Aig_ManFanoutStop( pAig ); if ( p->pPars->fUpdateLevel ) + { +// Aig_ManVerifyReverseLevel( pAig ); Aig_ManStopReverseLevels( pAig ); + } // stop the rewriting manager Dar_ManStop( p ); // check @@ -183,28 +203,25 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval; SeeAlso [] ***********************************************************************/ -Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig ) +Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax ) { Dar_Man_t * p; + Dar_RwrPar_t Pars, * pPars = &Pars; Aig_Obj_t * pObj; Aig_MmFixed_t * pMemCuts; int i, clk = 0, clkStart = clock(); - int nCutsMax = 0, nCutsTotal = 0; - // create rewriting manager - p = Dar_ManStart( pAig, NULL ); // remove dangling nodes Aig_ManCleanup( pAig ); + // create default parameters + Dar_ManDefaultRwrParams( pPars ); + pPars->nCutsMax = nCutsMax; + // create rewriting manager + p = Dar_ManStart( pAig, pPars ); // set elementary cuts for the PIs Dar_ManCutsStart( p ); // compute cuts for each nodes in the topological order - Aig_ManForEachObj( pAig, pObj, i ) - { - if ( !Aig_ObjIsNode(pObj) ) - continue; + Aig_ManForEachNode( pAig, pObj, i ) Dar_ObjComputeCuts( p, pObj ); - nCutsTotal += pObj->nCuts - 1; - nCutsMax = AIG_MAX( nCutsMax, (int)pObj->nCuts - 1 ); - } // free the cuts pMemCuts = p->pMemCuts; p->pMemCuts = NULL; diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h index 0acd272c..b14d5c30 100644 --- a/src/aig/dar/darInt.h +++ b/src/aig/dar/darInt.h @@ -55,7 +55,8 @@ struct Dar_Cut_t_ // 6 words { unsigned uSign; // cut signature unsigned uTruth : 16; // the truth table of the cut function - unsigned Value : 12; // the value of the cut + unsigned Value : 11; // the value of the cut + unsigned fBest : 1; // marks the best cut unsigned fUsed : 1; // marks the cut currently in use unsigned nLeaves : 3; // the number of leaves int pLeaves[4]; // the array of leaves @@ -85,6 +86,7 @@ struct Dar_Man_t_ int nCutMemUsed; // memory used for cuts // rewriting statistics int nNodesInit; // the original number of nodes + int nNodesTried; // the number of nodes attempted int nCutsAll; // all cut pairs int nCutsTried; // computed cuts int nCutsUsed; // used cuts diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c index 72ce0cde..e159f35a 100644 --- a/src/aig/dar/darLib.c +++ b/src/aig/dar/darLib.c @@ -798,9 +798,13 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class ) pFanin0 = Aig_NotCond( pData0->pFunc, pObj->fCompl0 ); pFanin1 = Aig_NotCond( pData1->pFunc, pObj->fCompl1 ); 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; + if ( pData->pFunc ) + { + // update the level to be more accurate + pData->Level = Aig_Regular(pData->pFunc)->Level; + // mark the node if it is part of MFFC + pData->fMffc = Aig_ObjIsTravIdCurrent(p->pAig, pData->pFunc); + } } } @@ -823,10 +827,10 @@ int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required return 0; assert( pObj->Num > 3 ); pData = s_DarLib->pDatas + pObj->Num; - if ( pData->pFunc && !pData->fMffc ) - return 0; if ( pData->Level > Required ) return 0xff; + if ( pData->pFunc && !pData->fMffc ) + return 0; if ( pData->TravId == Out ) return 0; pData->TravId = Out; @@ -894,6 +898,7 @@ void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir p->LevelBest = s_DarLib->pDatas[pObj->Num].Level; p->GainBest = nNodesGained; p->ClassBest = Class; + assert( p->LevelBest <= Required ); } clk = clock() - clk; p->ClassTimes[Class] += clk; @@ -943,6 +948,7 @@ Aig_Obj_t * Dar_LibBuildBest_rec( Dar_Man_t * p, Dar_LibObj_t * pObj ) pFanin0 = Aig_NotCond( pFanin0, pObj->fCompl0 ); pFanin1 = Aig_NotCond( pFanin1, pObj->fCompl1 ); pData->pFunc = Aig_And( p->pAig, pFanin0, pFanin1 ); +// assert( pData->Level == (int)Aig_Regular(pData->pFunc)->Level ); return pData->pFunc; } diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c index ef898ea2..155d48bd 100644 --- a/src/aig/dar/darMan.c +++ b/src/aig/dar/darMan.c @@ -94,14 +94,14 @@ void Dar_ManPrintStats( Dar_Man_t * p ) extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ); Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig); - printf( "NodesBeg = %8d. NodesEnd = %8d. Gain = %6d. (%6.2f %%). Cut mem = %d Mb\n", - p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit, p->nCutMemUsed ); + printf( "Tried = %8d. Beg = %8d. End = %8d. Gain = %6d. (%6.2f %%). Cut mem = %d Mb\n", + p->nNodesTried, p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit, p->nCutMemUsed ); printf( "Cuts = %8d. Tried = %8d. Used = %8d. Bad = %5d. Skipped = %5d. Ave = %.2f.\n", p->nCutsAll, p->nCutsTried, p->nCutsUsed, p->nCutsBad, p->nCutsSkipped, (float)p->nCutsUsed/Aig_ManNodeNum(p->pAig) ); - printf( "Bufs = %5d. BufMax = %5d. BufReplace = %6d. BufFix = %6d.\n", - Aig_ManBufNum(p->pAig), p->pAig->nBufMax, p->pAig->nBufReplaces, p->pAig->nBufFixes ); + printf( "Bufs = %5d. BufMax = %5d. BufReplace = %6d. BufFix = %6d. Levels = %4d.\n", + Aig_ManBufNum(p->pAig), p->pAig->nBufMax, p->pAig->nBufReplaces, p->pAig->nBufFixes, Aig_ManLevels(p->pAig) ); PRT( "Cuts ", p->timeCuts ); PRT( "Eval ", p->timeEval ); PRT( "Other ", p->timeOther ); diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c index cdfbaa01..fbd12cae 100644 --- a/src/aig/dar/darRefact.c +++ b/src/aig/dar/darRefact.c @@ -130,8 +130,8 @@ 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 ); + printf( "Tried = %6d. Below = %5d. Extended = %5d. Used = %5d. Levels = %4d.\n", + p->nNodesTried, p->nNodesBelow, p->nNodesExten, p->nCutsUsed, Aig_ManLevels(p->pAig) ); PRT( "Cuts ", p->timeCuts ); PRT( "Eval ", p->timeEval ); PRT( "Other ", p->timeOther ); @@ -358,7 +358,7 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in p->nCutsTried++; // get the cut nodes - Aig_ManCollectCut( pObj, vCut, p->vCutNodes ); + Aig_ObjCollectCut( pObj, vCut, p->vCutNodes ); // get the truth table pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore ); // try the positive phase @@ -460,7 +460,7 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars ) // remove dangling nodes Aig_ManCleanup( pAig ); // if updating levels is requested, start fanout and timing - Aig_ManCreateFanout( pAig ); + Aig_ManFanoutStart( pAig ); if ( p->pPars->fUpdateLevel ) Aig_ManStartReverseLevels( pAig, 0 ); @@ -480,11 +480,6 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars ) 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(); @@ -558,7 +553,7 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval; // put the nodes into the DFS order and reassign their IDs // Aig_NtkReassignIds( p ); // fix the levels - Aig_ManDeleteFanout( pAig ); + Aig_ManFanoutStop( pAig ); if ( p->pPars->fUpdateLevel ) Aig_ManStopReverseLevels( pAig ); diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c index 8423a4e6..75076981 100644 --- a/src/aig/dar/darScript.c +++ b/src/aig/dar/darScript.c @@ -39,11 +39,10 @@ SeeAlso [] ***********************************************************************/ -Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose ) +Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, 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; @@ -51,12 +50,18 @@ Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose ) Dar_ManDefaultRwrParams( pParsRwr ); Dar_ManDefaultRefParams( pParsRef ); + pParsRwr->fUpdateLevel = fUpdateLevel; + pParsRef->fUpdateLevel = fUpdateLevel; + pParsRwr->fVerbose = fVerbose; pParsRef->fVerbose = fVerbose; // balance - pAig = Dar_ManBalance( pTemp = pAig, fBalance ); - Aig_ManStop( pTemp ); + if ( fBalance ) + { +// pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); +// Aig_ManStop( pTemp ); + } // rewrite Dar_ManRewrite( pAig, pParsRwr ); @@ -69,8 +74,11 @@ Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose ) Aig_ManStop( pTemp ); // balance - pAig = Dar_ManBalance( pTemp = pAig, fBalance ); +// if ( fBalance ) + { + pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); Aig_ManStop( pTemp ); + } // rewrite Dar_ManRewrite( pAig, pParsRwr ); @@ -86,8 +94,11 @@ Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose ) Aig_ManStop( pTemp ); // balance - pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + if ( fBalance ) + { + pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); Aig_ManStop( pTemp ); + } // refactor Dar_ManRefactor( pAig, pParsRef ); @@ -100,8 +111,11 @@ Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose ) Aig_ManStop( pTemp ); // balance - pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + if ( fBalance ) + { + pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); Aig_ManStop( pTemp ); + } return pAig; } @@ -116,11 +130,10 @@ Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose ) 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 * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ) +//alias rwsat "st; rw -l; b -l; rw -l; rf -l" { Aig_Man_t * pTemp; - int fBalance = 0; Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; Dar_RefPar_t ParsRef, * pParsRef = &ParsRef; @@ -128,71 +141,8 @@ Aig_Man_t * Dar_ManCompress2_no_z( Aig_Man_t * pAig, int fVerbose ) 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->fUpdateLevel = 0; + pParsRef->fUpdateLevel = 0; pParsRwr->fVerbose = fVerbose; pParsRef->fVerbose = fVerbose; @@ -206,37 +156,19 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fVerbose ) 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 ); + if ( fBalance ) + { + pAig = Dar_ManBalance( 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/fra/fra.h b/src/aig/fra/fra.h index 7f2df105..127882ea 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -60,6 +60,7 @@ struct Fra_Par_t_ int MaxScore; // max score after which resimulation is used double dActConeRatio; // the ratio of cone to be bumped double dActConeBumpMax; // the largest bump in activity + int fChoicing; // enables choicing int fSpeculate; // use speculative reduction int fProve; // prove the miter outputs int fVerbose; // verbose output @@ -101,6 +102,7 @@ struct Fra_Man_t_ // various data members Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes Aig_Obj_t ** pMemRepr; // memory allocated for points to the node representatives + Aig_Obj_t ** pMemReprFra; // memory allocated for points to the node representatives in the FRAIG Vec_Ptr_t ** pMemFanins; // the arrays of fanins int * pMemSatNums; // the array of SAT numbers int nSizeAlloc; // allocated size of the arrays @@ -118,7 +120,9 @@ struct Fra_Man_t_ int nSatProof; int nSatFails; int nSatFailsReal; - int nSpeculs; + int nSpeculs; + int nChoices; + int nChoicesFake; // runtime int timeSim; int timeTrav; @@ -141,11 +145,13 @@ static inline unsigned Fra_ObjRandomSim() { return (rand() << static inline Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]; } static inline Aig_Obj_t * Fra_ObjRepr( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]; } +static inline Aig_Obj_t * Fra_ObjReprFra( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemReprFra[pObj->Id]; } static inline Vec_Ptr_t * Fra_ObjFaninVec( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; } static inline int Fra_ObjSatNum( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; } static inline void Fra_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id] = pNode; } static inline void Fra_ObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id] = pNode; } +static inline void Fra_ObjSetReprFra( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemReprFra[pObj->Id] = pNode; } static inline void Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; } static inline void Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; } @@ -160,8 +166,6 @@ static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_I /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== fraAnd.c ========================================================*/ -extern void Fra_Sweep( Fra_Man_t * p ); /*=== fraClass.c ========================================================*/ extern void Fra_PrintClasses( Fra_Man_t * p ); extern void Fra_CreateClasses( Fra_Man_t * p ); @@ -170,7 +174,10 @@ extern int Fra_RefineClasses1( Fra_Man_t * p ); /*=== fraCnf.c ========================================================*/ extern void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); /*=== fraCore.c ========================================================*/ -extern Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pParams ); +extern Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars ); +extern Aig_Man_t * Fra_Choice( Aig_Man_t * pManAig ); +/*=== fraDfs.c ========================================================*/ +extern int Fra_CheckTfi( Fra_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld ); /*=== fraMan.c ========================================================*/ extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams ); diff --git a/src/aig/fra/fraAnd.c b/src/aig/fra/fraAnd.c deleted file mode 100644 index 36b4ccc3..00000000 --- a/src/aig/fra/fraAnd.c +++ /dev/null @@ -1,156 +0,0 @@ -/**CFile**************************************************************** - - FileName [fraAnd.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Fraig FRAIG package.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 30, 2007.] - - Revision [$Id: fraAnd.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "fra.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - - -/**Function************************************************************* - - Synopsis [Performs fraiging for one node.] - - Description [Returns the fraiged node.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld ) -{ - Aig_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig; - int RetValue; - assert( !Aig_IsComplement(pObjOld) ); - assert( Aig_ObjIsNode(pObjOld) ); - // get the fraiged fanins - pFanin0Fraig = Fra_ObjChild0Fra(pObjOld); - pFanin1Fraig = Fra_ObjChild1Fra(pObjOld); - // get the fraiged node - pObjFraig = Aig_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig ); - if ( Aig_ObjIsConst1(Aig_Regular(pObjFraig)) ) - return pObjFraig; - Aig_Regular(pObjFraig)->pData = p; - // get representative of this class - pObjOldRepr = Fra_ObjRepr(pObjOld); - if ( pObjOldRepr == NULL || // this is a unique node - (!p->pPars->fDoSparse && pObjOldRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node - { - assert( Aig_Regular(pFanin0Fraig) != Aig_Regular(pFanin1Fraig) ); - assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin0Fraig) ); - assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin1Fraig) ); - return pObjFraig; - } - // get the fraiged representative - pObjOldReprFraig = Fra_ObjFraig(pObjOldRepr); - // if the fraiged nodes are the same, return - if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjOldReprFraig) ) - return pObjFraig; - assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) ); -// printf( "Node = %d. Repr = %d.\n", pObjOld->Id, pObjOldRepr->Id ); - - // if they are proved different, the c-ex will be in p->pPatWords - RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) ); - if ( RetValue == 1 ) // proved equivalent - { -// pObjOld->fMarkA = 1; - return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase ); - } - if ( RetValue == -1 ) // failed - { - Aig_Obj_t * ppNodes[2] = { Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) }; - Vec_Ptr_t * vNodes; - - if ( !p->pPars->fSpeculate ) - return pObjFraig; - // substitute the node -// pObjOld->fMarkB = 1; - p->nSpeculs++; - - vNodes = Aig_ManDfsNodes( p->pManFraig, ppNodes, 2 ); - printf( "%d ", Vec_PtrSize(vNodes) ); - Vec_PtrFree( vNodes ); - - return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase ); - } -// printf( "Disproved %d and %d.\n", pObjOldRepr->Id, pObjOld->Id ); - // simulate the counter-example and return the Fraig node -// printf( "Representaive before = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 ); - Fra_Resimulate( p ); -// printf( "Representaive after = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 ); - assert( Fra_ObjRepr(pObjOld) != pObjOldRepr ); - return pObjFraig; -} - -/**Function************************************************************* - - Synopsis [Performs fraiging for the internal nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_Sweep( Fra_Man_t * p ) -{ - Aig_Obj_t * pObj, * pObjNew; - int i, k = 0; -p->nClassesZero = Vec_PtrSize(p->vClasses1); -p->nClassesBeg = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0); - // duplicate internal nodes -// p->pProgress = Extra_ProgressBarStart( stdout, Aig_ManNodeNum(p->pManAig) ); - Aig_ManForEachNode( p->pManAig, pObj, i ) - { -// Extra_ProgressBarUpdate( p->pProgress, k++, NULL ); - // default to simple strashing if simulation detected a counter-example for a PO - if ( p->pManFraig->pData ) - pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) ); - else - pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented - Fra_ObjSetFraig( pObj, pObjNew ); - assert( Fra_ObjFraig(pObj) != NULL ); - } -// Extra_ProgressBarStop( p->pProgress ); -p->nClassesEnd = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0); - // try to prove the outputs of the miter - p->nNodesMiter = Aig_ManNodeNum(p->pManFraig); -// Fra_MiterStatus( p->pManFraig ); -// if ( p->pPars->fProve && p->pManFraig->pData == NULL ) -// Fra_MiterProve( p ); - // add the POs - Aig_ManForEachPo( p->pManAig, pObj, i ) - Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) ); - // remove dangling nodes - Aig_ManCleanup( p->pManFraig ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index 9e1a9a1a..ca2d0fb4 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -30,6 +30,177 @@ /**Function************************************************************* + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld ) +{ + Aig_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig; + int RetValue; + assert( !Aig_IsComplement(pObjOld) ); + assert( Aig_ObjIsNode(pObjOld) ); + // get the fraiged fanins + pFanin0Fraig = Fra_ObjChild0Fra(pObjOld); + pFanin1Fraig = Fra_ObjChild1Fra(pObjOld); + // get the fraiged node + pObjFraig = Aig_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig ); + if ( Aig_ObjIsConst1(Aig_Regular(pObjFraig)) ) + return pObjFraig; + Aig_Regular(pObjFraig)->pData = p; + // get representative of this class + pObjOldRepr = Fra_ObjRepr(pObjOld); + if ( pObjOldRepr == NULL || // this is a unique node + (!p->pPars->fDoSparse && pObjOldRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node + { + assert( Aig_Regular(pFanin0Fraig) != Aig_Regular(pFanin1Fraig) ); + assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin0Fraig) ); + assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin1Fraig) ); + return pObjFraig; + } + // get the fraiged representative + pObjOldReprFraig = Fra_ObjFraig(pObjOldRepr); + // if the fraiged nodes are the same, return + if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjOldReprFraig) ) + return pObjFraig; + assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) ); +// printf( "Node = %d. Repr = %d.\n", pObjOld->Id, pObjOldRepr->Id ); + + // if they are proved different, the c-ex will be in p->pPatWords + RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) ); + if ( RetValue == 1 ) // proved equivalent + { +// pObjOld->fMarkA = 1; + if ( p->pPars->fChoicing && !Fra_CheckTfi( p, Aig_Regular(pObjFraig), Aig_Regular(pObjOldReprFraig) ) ) + { +// Fra_ObjSetReprFra( Aig_Regular(pObjFraig), Aig_Regular(pObjOldReprFraig) ); + Aig_Obj_t * pObjNew = Aig_Regular(pObjFraig); + Aig_Obj_t * pObjOld = Aig_Regular(pObjOldReprFraig); + Aig_Obj_t * pTemp; + assert( pObjNew != pObjOld ); + for ( pTemp = Fra_ObjReprFra(pObjOld); pTemp; pTemp = Fra_ObjReprFra(pTemp) ) + if ( pTemp == pObjNew ) + break; + if ( pTemp == NULL ) + { + Fra_ObjSetReprFra( pObjNew, Fra_ObjReprFra(pObjOld) ); + Fra_ObjSetReprFra( pObjOld, pObjNew ); + assert( pObjOld != Fra_ObjReprFra(pObjOld) ); + assert( pObjNew != Fra_ObjReprFra(pObjNew) ); + p->nChoices++; + + assert( pObjOld->Id < pObjNew->Id ); + } + else + p->nChoicesFake++; + } + return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase ); + } + if ( RetValue == -1 ) // failed + { + static int Counter = 0; + char FileName[20]; + Aig_Man_t * pTemp; + Aig_Obj_t * pObj; + int i; + + Aig_Obj_t * ppNodes[2] = { Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) }; +// Vec_Ptr_t * vNodes; + + if ( !p->pPars->fSpeculate ) + return pObjFraig; + // substitute the node +// pObjOld->fMarkB = 1; + p->nSpeculs++; + + pTemp = Aig_ManExtractMiter( p->pManFraig, ppNodes, 2 ); + sprintf( FileName, "aig\\%03d.blif", ++Counter ); + Aig_ManDumpBlif( pTemp, FileName ); + printf( "Speculation cone with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(pTemp), FileName ); + Aig_ManStop( pTemp ); + + Aig_ManForEachObj( p->pManFraig, pObj, i ) + pObj->pData = p; + +// vNodes = Aig_ManDfsNodes( p->pManFraig, ppNodes, 2 ); +// printf( "Cone=%d ", Vec_PtrSize(vNodes) ); +// Vec_PtrFree( vNodes ); + + return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase ); + } +// printf( "Disproved %d and %d.\n", pObjOldRepr->Id, pObjOld->Id ); + // simulate the counter-example and return the Fraig node +// printf( "Representaive before = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 ); + Fra_Resimulate( p ); +// printf( "Representaive after = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 ); + assert( Fra_ObjRepr(pObjOld) != pObjOldRepr ); + return pObjFraig; +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_Sweep( Fra_Man_t * p ) +{ + ProgressBar * pProgress; + Aig_Obj_t * pObj, * pObjNew; + int i, k = 0; +p->nClassesZero = Vec_PtrSize(p->vClasses1); +p->nClassesBeg = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0); + // duplicate internal nodes + pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) ); + Aig_ManForEachNode( p->pManAig, pObj, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + // default to simple strashing if simulation detected a counter-example for a PO + if ( p->pManFraig->pData ) + pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) ); + else + pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented + Fra_ObjSetFraig( pObj, pObjNew ); + assert( Fra_ObjFraig(pObj) != NULL ); + } + Extra_ProgressBarStop( pProgress ); +p->nClassesEnd = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0); + // try to prove the outputs of the miter + p->nNodesMiter = Aig_ManNodeNum(p->pManFraig); +// Fra_MiterStatus( p->pManFraig ); +// if ( p->pPars->fProve && p->pManFraig->pData == NULL ) +// Fra_MiterProve( p ); + // add the POs + Aig_ManForEachPo( p->pManAig, pObj, i ) + Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) ); + // postprocess + Aig_ManCleanMarkB( p->pManFraig ); + if ( p->pPars->fChoicing ) + { + // transfer the representative info + p->pManFraig->pReprs = p->pMemReprFra; + p->pMemReprFra = NULL; +// printf( "The number of choices = %d. Fake choices = %d.\n", p->nChoices, p->nChoicesFake ); + } + else + { + // remove dangling nodes + Aig_ManCleanup( p->pManFraig ); + } +} + +/**Function************************************************************* + Synopsis [Performs fraiging of the AIG.] Description [] @@ -57,6 +228,30 @@ p->timeTotal = clock() - clk; return pManAigNew; } +/**Function************************************************************* + + Synopsis [Performs choicing of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Fra_Choice( Aig_Man_t * pManAig ) +{ + Fra_Par_t Pars, * pPars = &Pars; + Fra_ParamsDefault( pPars ); + pPars->nBTLimitNode = 1000; + pPars->fVerbose = 0; + pPars->fProve = 0; + pPars->fDoSparse = 1; + pPars->fSpeculate = 0; + pPars->fChoicing = 1; + return Fra_Perform( pManAig, pPars ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraDfs.c b/src/aig/fra/fraDfs.c new file mode 100644 index 00000000..cd0985e0 --- /dev/null +++ b/src/aig/fra/fraDfs.c @@ -0,0 +1,87 @@ +/**CFile**************************************************************** + + FileName [fraDfs.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fraig FRAIG package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 30, 2007.] + + Revision [$Id: fraDfs.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "fra.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_CheckTfi_rec( Fra_Man_t * p, Aig_Obj_t * pNode, Aig_Obj_t * pOld ) +{ + // check the trivial cases + if ( pNode == NULL ) + return 0; +// if ( pNode->Id < pOld->Id ) // cannot use because of choicesof pNode +// return 0; + if ( pNode == pOld ) + return 1; + // skip the visited node + if ( Aig_ObjIsTravIdCurrent(p->pManFraig, pNode) ) + return 0; + Aig_ObjSetTravIdCurrent(p->pManFraig, pNode); + // check the children + if ( Fra_CheckTfi_rec( p, Aig_ObjFanin0(pNode), pOld ) ) + return 1; + if ( Fra_CheckTfi_rec( p, Aig_ObjFanin1(pNode), pOld ) ) + return 1; + // check equivalent nodes + return Fra_CheckTfi_rec( p, Fra_ObjReprFra(pNode), pOld ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_CheckTfi( Fra_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld ) +{ + assert( !Aig_IsComplement(pNew) ); + assert( !Aig_IsComplement(pOld) ); + Aig_ManIncrementTravId( p->pManFraig ); + return Fra_CheckTfi_rec( p, pNew, pOld ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index 78246a8c..0e583d6c 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -97,6 +97,8 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars ) memset( p->pMemFraig, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) ); p->pMemRepr = ALLOC( Aig_Obj_t *, p->nSizeAlloc ); memset( p->pMemRepr, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) ); + p->pMemReprFra = ALLOC( Aig_Obj_t *, p->nSizeAlloc ); + memset( p->pMemReprFra, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) ); p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc ); memset( p->pMemFanins, 0, p->nSizeAlloc * sizeof(Vec_Ptr_t *) ); p->pMemSatNums = ALLOC( int, p->nSizeAlloc ); @@ -166,6 +168,7 @@ void Fra_ManStop( Fra_Man_t * p ) FREE( p->pMemSatNums ); FREE( p->pMemFanins ); FREE( p->pMemRepr ); + FREE( p->pMemReprFra ); FREE( p->pMemFraig ); FREE( p->pMemClasses ); FREE( p->pPatScores ); diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c index 66b1ba5a..8ab10c40 100644 --- a/src/aig/fra/fraSat.c +++ b/src/aig/fra/fraSat.c @@ -54,8 +54,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) // if the backtrack limit is small, simply skip this node // if the backtrack limit is > 10, take the quare root of the limit nBTLimit = p->pPars->nBTLimitNode; -/* - if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) ) + if ( !p->pPars->fSpeculate && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) ) { p->nSatFails++; // fail immediately @@ -64,7 +63,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) return -1; nBTLimit = (int)pow(nBTLimit, 0.7); } -*/ + p->nSatCalls++; // make sure the solver is allocated and has enough variables @@ -112,9 +111,9 @@ p->timeSatSat += clock() - clk; { p->timeSatFail += clock() - clk; // mark the node as the failed node -// if ( pOld != p->pManFraig->pConst1 ) -// pOld->fFailTfo = 1; -// pNew->fFailTfo = 1; + if ( pOld != p->pManFraig->pConst1 ) + pOld->fMarkB = 1; + pNew->fMarkB = 1; p->nSatFailsReal++; return -1; } @@ -155,8 +154,8 @@ p->timeSatSat += clock() - clk; { p->timeSatFail += clock() - clk; // mark the node as the failed node -// pOld->fFailTfo = 1; -// pNew->fFailTfo = 1; + pOld->fMarkB = 1; + pNew->fMarkB = 1; p->nSatFailsReal++; return -1; } @@ -240,7 +239,7 @@ p->timeSatSat += clock() - clk; { p->timeSatFail += clock() - clk; // mark the node as the failed node -// pNew->fFailTfo = 1; + pNew->fMarkB = 1; p->nSatFailsReal++; return -1; } diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make index 934fbdac..df690700 100644 --- a/src/aig/fra/module.make +++ b/src/aig/fra/module.make @@ -1,7 +1,7 @@ -SRC += src/aig/fra/fraAnd.c \ - src/aig/fra/fraClass.c \ +SRC += src/aig/fra/fraClass.c \ src/aig/fra/fraCnf.c \ src/aig/fra/fraCore.c \ + src/aig/fra/fraDfs.c \ src/aig/fra/fraMan.c \ src/aig/fra/fraSat.c \ src/aig/fra/fraSim.c diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index faa2fe2e..bda8781c 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -234,6 +234,7 @@ struct Abc_Lib_t_ // maximum/minimum operators #define ABC_MIN(a,b) (((a) < (b))? (a) : (b)) #define ABC_MAX(a,b) (((a) > (b))? (a) : (b)) +#define ABC_ABS(a) (((a) >= 0)? (a) :-(a)) #define ABC_INFINITY (100000000) // transforming floats into ints and back diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6b32cd43..1dd9b65e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -92,6 +92,7 @@ static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTopmost ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -113,6 +114,7 @@ static int Abc_CommandIRewrite ( Abc_Frame_t * pAbc, int argc, char ** arg 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_CommandDrwsat ( 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 ); @@ -169,6 +171,7 @@ static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -252,6 +255,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 ); Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandCone, 1 ); Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandNode, 1 ); + Cmd_CommandAdd( pAbc, "Various", "topmost", Abc_CommandTopmost, 1 ); Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 ); Cmd_CommandAdd( pAbc, "Various", "exdc_free", Abc_CommandExdcFree, 1 ); Cmd_CommandAdd( pAbc, "Various", "exdc_get", Abc_CommandExdcGet, 1 ); @@ -273,6 +277,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) 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", "drwsat", Abc_CommandDrwsat, 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 ); @@ -329,6 +334,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 ); Cmd_CommandAdd( pAbc, "Verification", "debug", Abc_CommandDebug, 0 ); @@ -5032,6 +5038,95 @@ usage: } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandTopmost( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c, nLevels; + extern Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nLevels = 10; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nLevels = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLevels < 0 ) + goto usage; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); + return 0; + } + + if ( Abc_NtkLatchNum(pNtk) > 0 ) + { + fprintf( stdout, "Currently can only works for combinational circuits.\n" ); + return 0; + } + if ( Abc_NtkPoNum(pNtk) != 1 ) + { + fprintf( stdout, "Currently expects a single-output miter.\n" ); + return 0; + } + + pNtkRes = Abc_NtkTopmost( pNtk, nLevels ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "The command has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: topmost [-N num] [-h]\n" ); + fprintf( pErr, "\t replaces the current network by several of its topmost levels\n" ); + fprintf( pErr, "\t-N num : max number of levels [default = %d]\n", nLevels ); + fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\tname : the node name\n"); + return 1; +} + /**Function************************************************************* @@ -6098,9 +6193,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Network should be strashed. Command has failed.\n" ); return 1; } - pNtkRes = Abc_NtkDar( pNtk ); -// pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" ); - pNtkRes = NULL; +// pNtkRes = Abc_NtkDar( pNtk ); + pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" ); +// pNtkRes = NULL; if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -6635,7 +6730,7 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Dar_ManDefaultRwrParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CNlzvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CNflzvwh" ) ) != EOF ) { switch ( c ) { @@ -6661,6 +6756,9 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nSubgMax < 0 ) goto usage; break; + case 'f': + pPars->fFanout ^= 1; + break; case 'l': pPars->fUpdateLevel ^= 1; break; @@ -6695,10 +6793,11 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: drw [-C num] [-N num] [-lzvwh]\n" ); + fprintf( pErr, "usage: drw [-C num] [-N num] [-flzvwh]\n" ); 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-f : toggle representing fanouts [default = %s]\n", pPars->fFanout? "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" ); @@ -6842,21 +6941,29 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; - int fVerbose, c; + int fBalance, fVerbose, fUpdateLevel, c; - extern Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + fBalance = 0; fVerbose = 0; + fUpdateLevel = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "blvh" ) ) != EOF ) { switch ( c ) { + case 'b': + fBalance ^= 1; + break; + case 'l': + fUpdateLevel ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -6871,7 +6978,7 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } - pNtkRes = Abc_NtkDCompress2( pNtk, fVerbose ); + pNtkRes = Abc_NtkDCompress2( pNtk, fBalance, fUpdateLevel, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -6882,8 +6989,77 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dcompress2 [-vh]\n" ); + fprintf( pErr, "usage: dcompress2 [-blvh]\n" ); fprintf( pErr, "\t performs combinational AIG optimization\n" ); + fprintf( pErr, "\t-b : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" ); + fprintf( pErr, "\t-l : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" ); + 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_CommandDrwsat( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int fBalance, fVerbose, c; + + extern Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fBalance = 0; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "bvh" ) ) != EOF ) + { + switch ( c ) + { + case 'b': + fBalance ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + pNtkRes = Abc_NtkDrwsat( pNtk, fBalance, 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: drwsat [-bvh]\n" ); + fprintf( pErr, "\t performs combinational AIG optimization for SAT\n" ); + fprintf( pErr, "\t-b : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -7212,10 +7388,9 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; - int c, fProve, fVerbose, fDoSparse, fSpeculate; - int nConfLimit; + int c, nConfLimit, fDoSparse, fProve, fSpeculate, fChoicing, fVerbose; - extern Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fChoicing, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -7223,12 +7398,13 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nConfLimit = 100; - fSpeculate = 0; fDoSparse = 1; fProve = 0; + fSpeculate = 0; + fChoicing = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Csprvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Csprcvh" ) ) != EOF ) { switch ( c ) { @@ -7252,6 +7428,9 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': fSpeculate ^= 1; break; + case 'c': + fChoicing ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -7267,7 +7446,7 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fSpeculate, fVerbose ); + pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fSpeculate, fChoicing, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -7278,12 +7457,13 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dfraig [-C num] [-sprvh]\n" ); + fprintf( pErr, "usage: dfraig [-C num] [-sprcvh]\n" ); fprintf( pErr, "\t performs fraiging using a new method\n" ); fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); fprintf( pErr, "\t-s : toggle considering sparse functions [default = %s]\n", fDoSparse? "yes": "no" ); fprintf( pErr, "\t-p : toggle proving the miter outputs [default = %s]\n", fProve? "yes": "no" ); fprintf( pErr, "\t-r : toggle speculative reduction [default = %s]\n", fSpeculate? "yes": "no" ); + fprintf( pErr, "\t-c : toggle accumulation of choices [default = %s]\n", fChoicing? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -7836,7 +8016,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pParams->fFuncRed = 1; // performs only one level hashing pParams->fFeedBack = 1; // enables solver feedback pParams->fDist1Pats = 1; // enables distance-1 patterns - pParams->fDoSparse = 0; // performs equiv tests for sparse functions + pParams->fDoSparse = 1; // performs equiv tests for sparse functions pParams->fChoicing = 0; // enables recording structural choices pParams->fTryProve = 0; // tries to solve the final miter pParams->fVerbose = 0; // the verbosiness flag @@ -11327,6 +11507,142 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int RetValue; + int fVerbose; + int nConfLimit; + int nInsLimit; + int clk; + + extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose ); + + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fVerbose = 0; + nConfLimit = 100000; + nInsLimit = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLimit < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nInsLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nInsLimit < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkLatchNum(pNtk) > 0 ) + { + fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" ); + return 0; + } + if ( Abc_NtkPoNum(pNtk) != 1 ) + { + fprintf( stdout, "Currently expects a single-output miter.\n" ); + return 0; + } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); + return 0; + } + + clk = clock(); + RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fVerbose ); + // verify that the pattern is correct + if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 ) + { + //int i; + //Abc_Obj_t * pObj; + int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtk->pModel ); + if ( pSimInfo[0] != 1 ) + printf( "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" ); + free( pSimInfo ); + /* + // print model + Abc_NtkForEachPi( pNtk, pObj, i ) + { + printf( "%d", (int)(pNtk->pModel[i] > 0) ); + if ( i == 70 ) + break; + } + printf( "\n" ); + */ + } + + if ( RetValue == -1 ) + printf( "UNDECIDED " ); + else if ( RetValue == 0 ) + printf( "SATISFIABLE " ); + else + printf( "UNSATISFIABLE " ); + //printf( "\n" ); + PRT( "Time", clock() - clk ); + return 0; + +usage: + fprintf( pErr, "usage: dsat [-C num] [-I num] [-vh]\n" ); + fprintf( pErr, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" ); + fprintf( pErr, "\t derives CNF from the current network and leave it unchanged\n" ); + fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); + fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit ); + fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandProve( 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 bc47e2dc..f04f3d97 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -123,6 +123,69 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) SeeAlso [] ***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Aig_Obj_t * pObj, * pTemp; + int i; + assert( pMan->pReprs != NULL ); + assert( Aig_ManBufNum(pMan) == 0 ); + // perform strashing + pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // transfer the pointers to the basic nodes + Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); + Aig_ManForEachPi( pMan, pObj, i ) + pObj->pData = Abc_NtkCi(pNtkNew, i); + // rebuild the AIG + vNodes = Aig_ManDfsChoices( pMan ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) ); + if ( pTemp = pMan->pReprs[pObj->Id] ) + { + Abc_Obj_t * pAbcRepr, * pAbcObj; + assert( pTemp->pData != NULL ); + pAbcRepr = pObj->pData; + pAbcObj = pTemp->pData; + pAbcObj->pData = pAbcRepr->pData; + pAbcRepr->pData = pAbcObj; + } + } +printf( "Total = %d. Collected = %d.\n", Aig_ManNodeNum(pMan), Vec_PtrSize(vNodes) ); + Vec_PtrFree( vNodes ); +/* + { + Abc_Obj_t * pNode; + int k, Counter = 0; + Abc_NtkForEachNode( pNtkNew, pNode, k ) + if ( pNode->pData != 0 ) + { + int x = 0; + Counter++; + } + printf( "Choices = %d.\n", Counter ); + } +*/ + // connect the PO nodes + Aig_ManForEachPo( pMan, pObj, i ) + Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) { Vec_Ptr_t * vNodes; @@ -291,7 +354,7 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ) */ // Aig_ManDumpBlif( pMan, "aig_temp.blif" ); -// pMan->pPars = Dar_ManDefaultRwrParams(); +// pMan->pPars = Dar_ManDefaultRwrPars(); Dar_ManRewrite( pMan, NULL ); Aig_ManPrintStats( pMan ); // Dar_ManComputeCuts( pMan ); @@ -336,120 +399,31 @@ Aig_CnfFree( pCnf ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t * vMapped ) +Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fChoicing, int fVerbose ) { - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pNode, * pNodeNew; - Aig_Obj_t * pObj, * pLeaf; - Cnf_Cut_t * pCut; - Vec_Int_t * vCover; - unsigned uTruth; - int i, k, nDupGates; - // create the new network - pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); - // make the mapper point to the new network - Aig_ManConst1(p->pManAig)->pData = Abc_NtkCreateNodeConst1(pNtkNew); - Abc_NtkForEachCi( pNtk, pNode, i ) - Aig_ManPi(p->pManAig, i)->pData = pNode->pCopy; - // process the nodes in topological order - vCover = Vec_IntAlloc( 1 << 16 ); - Vec_PtrForEachEntry( vMapped, pObj, i ) - { - // create new node - pNodeNew = Abc_NtkCreateNode( pNtkNew ); - // add fanins according to the cut - pCut = pObj->pData; - Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k ) - Abc_ObjAddFanin( pNodeNew, pLeaf->pData ); - // add logic function - if ( pCut->nFanins < 5 ) - { - uTruth = 0xFFFF & *Cnf_CutTruth(pCut); - Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover ); - pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, vCover ); - } - else - pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] ); - // save the node - pObj->pData = pNodeNew; - } - Vec_IntFree( vCover ); - // add the CO drivers - Abc_NtkForEachCo( pNtk, pNode, i ) - { - pObj = Aig_ManPo(p->pManAig, i); - pNodeNew = Abc_ObjNotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); - Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); - } - - // remove the constant node if not used - pNodeNew = (Abc_Obj_t *)Aig_ManConst1(p->pManAig)->pData; - if ( Abc_ObjFanoutNum(pNodeNew) == 0 ) - Abc_NtkDeleteObj( pNodeNew ); - // minimize the node -// Abc_NtkSweep( pNtkNew, 0 ); - // decouple the PO driver nodes to reduce the number of levels - nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 ); -// if ( nDupGates && If_ManReadVerbose(pIfMan) ) -// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates ); - if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkConstructFromCnf(): Network check has failed.\n" ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Gives the current ABC network to AIG manager for processing.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) -{ - Abc_Ntk_t * pNtkNew = NULL; - Cnf_Man_t * pCnf; - Aig_Man_t * pMan; - Cnf_Dat_t * pData; - assert( Abc_NtkIsStrash(pNtk) ); - // convert to the AIG manager + Fra_Par_t Pars, * pPars = &Pars; + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; pMan = Abc_NtkToDar( pNtk ); if ( pMan == NULL ) return NULL; - if ( !Aig_ManCheck( pMan ) ) - { - printf( "Abc_NtkDarToCnf: AIG check has failed.\n" ); - Aig_ManStop( pMan ); - return NULL; - } - // perform balance - Aig_ManPrintStats( pMan ); - - // derive CNF - pCnf = Cnf_ManStart(); - pData = Cnf_Derive( pCnf, pMan ); - - { - Vec_Ptr_t * vMapped; - vMapped = Cnf_ManScanMapping( pCnf, 1 ); - pNtkNew = Abc_NtkConstructFromCnf( pNtk, pCnf, vMapped ); - Vec_PtrFree( vMapped ); - } - + Fra_ParamsDefault( pPars ); + pPars->nBTLimitNode = nConfLimit; + pPars->fVerbose = fVerbose; + pPars->fProve = fProve; + pPars->fDoSparse = fDoSparse; + pPars->fSpeculate = fSpeculate; + pPars->fChoicing = fChoicing; + pMan = Fra_Perform( pTemp = pMan, pPars ); + if ( fChoicing ) + pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan ); + else + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pTemp ); Aig_ManStop( pMan ); - Cnf_ManStop( pCnf ); - - // write CNF into a file -// Cnf_DataWriteIntoFile( pData, pFileName ); - Cnf_DataFree( pData ); - - return pNtkNew; + return pNtkAig; } - /**Function************************************************************* Synopsis [Gives the current ABC network to AIG manager for processing.] @@ -461,21 +435,15 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fVerbose ) +Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose ) { - Fra_Par_t Params, * pParams = &Params; + extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose ); Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; pMan = Abc_NtkToDar( pNtk ); if ( pMan == NULL ) return NULL; - Fra_ParamsDefault( pParams ); - pParams->nBTLimitNode = nConfLimit; - pParams->fVerbose = fVerbose; - pParams->fProve = fProve; - pParams->fDoSparse = fDoSparse; - pParams->fSpeculate = fSpeculate; - pMan = Fra_Perform( pTemp = pMan, pParams ); + pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose ); pNtkAig = Abc_NtkFromDar( pNtk, pMan ); Aig_ManStop( pTemp ); Aig_ManStop( pMan ); @@ -493,17 +461,35 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose ) +Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars ) { - extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose ); - Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; + Abc_Ntk_t * pNtkAig; + int clk; + assert( Abc_NtkIsStrash(pNtk) ); pMan = Abc_NtkToDar( pNtk ); if ( pMan == NULL ) return NULL; - pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose ); - pNtkAig = Abc_NtkFromDar( pNtk, pMan ); +// Aig_ManPrintStats( pMan ); + +// Aig_ManSupports( pMan ); + { + Vec_Vec_t * vParts; + vParts = Aig_ManPartitionSmart( pMan, 50, 1, NULL ); + Vec_VecFree( vParts ); + } + + Dar_ManRewrite( 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; } @@ -519,7 +505,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_RwrPar_t * pPars ) +Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars ) { Aig_Man_t * pMan, * pTemp; Abc_Ntk_t * pNtkAig; @@ -530,7 +516,7 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars ) return NULL; // Aig_ManPrintStats( pMan ); - Dar_ManRewrite( pMan, pPars ); + Dar_ManRefactor( pMan, pPars ); // pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel ); // Aig_ManStop( pTemp ); @@ -556,9 +542,9 @@ clk = clock(); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars ) +Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose ) { - Aig_Man_t * pMan, * pTemp; + Aig_Man_t * pMan;//, * pTemp; Abc_Ntk_t * pNtkAig; int clk; assert( Abc_NtkIsStrash(pNtk) ); @@ -567,13 +553,9 @@ Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars ) 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 ); + pMan = Dar_ManCompress2( pMan, fBalance, fUpdateLevel, fVerbose ); +// Aig_ManStop( pTemp ); //PRT( "time", clock() - clk ); // Aig_ManPrintStats( pMan ); @@ -593,7 +575,7 @@ clk = clock(); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fVerbose ) +Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose ) { Aig_Man_t * pMan;//, * pTemp; Abc_Ntk_t * pNtkAig; @@ -605,7 +587,7 @@ Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fVerbose ) // Aig_ManPrintStats( pMan ); clk = clock(); - pMan = Dar_ManCompress2( pMan, fVerbose ); + pMan = Dar_ManRwsat( pMan, fBalance, fVerbose ); // Aig_ManStop( pTemp ); //PRT( "time", clock() - clk ); @@ -615,6 +597,227 @@ clk = clock(); return pNtkAig; } +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t * vMapped ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pNode, * pNodeNew; + Aig_Obj_t * pObj, * pLeaf; + Cnf_Cut_t * pCut; + Vec_Int_t * vCover; + unsigned uTruth; + int i, k, nDupGates; + // create the new network + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); + // make the mapper point to the new network + Aig_ManConst1(p->pManAig)->pData = Abc_NtkCreateNodeConst1(pNtkNew); + Abc_NtkForEachCi( pNtk, pNode, i ) + Aig_ManPi(p->pManAig, i)->pData = pNode->pCopy; + // process the nodes in topological order + vCover = Vec_IntAlloc( 1 << 16 ); + Vec_PtrForEachEntry( vMapped, pObj, i ) + { + // create new node + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + // add fanins according to the cut + pCut = pObj->pData; + Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k ) + Abc_ObjAddFanin( pNodeNew, pLeaf->pData ); + // add logic function + if ( pCut->nFanins < 5 ) + { + uTruth = 0xFFFF & *Cnf_CutTruth(pCut); + Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover ); + pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, vCover ); + } + else + pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] ); + // save the node + pObj->pData = pNodeNew; + } + Vec_IntFree( vCover ); + // add the CO drivers + Abc_NtkForEachCo( pNtk, pNode, i ) + { + pObj = Aig_ManPo(p->pManAig, i); + pNodeNew = Abc_ObjNotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); + } + + // remove the constant node if not used + pNodeNew = (Abc_Obj_t *)Aig_ManConst1(p->pManAig)->pData; + if ( Abc_ObjFanoutNum(pNodeNew) == 0 ) + Abc_NtkDeleteObj( pNodeNew ); + // minimize the node +// Abc_NtkSweep( pNtkNew, 0 ); + // decouple the PO driver nodes to reduce the number of levels + nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 ); +// if ( nDupGates && If_ManReadVerbose(pIfMan) ) +// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkConstructFromCnf(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) +{ + Vec_Ptr_t * vMapped; + Aig_Man_t * pMan; + Cnf_Man_t * pManCnf; + Cnf_Dat_t * pCnf; + Abc_Ntk_t * pNtkNew = NULL; + assert( Abc_NtkIsStrash(pNtk) ); + + // convert to the AIG manager + pMan = Abc_NtkToDar( pNtk ); + if ( pMan == NULL ) + return NULL; + if ( !Aig_ManCheck( pMan ) ) + { + printf( "Abc_NtkDarToCnf: AIG check has failed.\n" ); + Aig_ManStop( pMan ); + return NULL; + } + // perform balance + Aig_ManPrintStats( pMan ); + + // derive CNF + pCnf = Cnf_Derive( pMan ); + pManCnf = Cnf_ManRead(); + + // write the network for verification + vMapped = Cnf_ManScanMapping( pManCnf, 1, 0 ); + pNtkNew = Abc_NtkConstructFromCnf( pNtk, pManCnf, vMapped ); + Vec_PtrFree( vMapped ); + + // write CNF into a file + Cnf_DataWriteIntoFile( pCnf, pFileName ); + Cnf_DataFree( pCnf ); + Cnf_ClearMemory(); + + Aig_ManStop( pMan ); + return pNtkNew; +} + + +/**Function************************************************************* + + Synopsis [Solves combinational miter using a SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose ) +{ + sat_solver * pSat; + Aig_Man_t * pMan; + Cnf_Dat_t * pCnf; + int status, RetValue, clk = clock(); + Vec_Int_t * vCiIds; + + assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkLatchNum(pNtk) == 0 ); + assert( Abc_NtkPoNum(pNtk) == 1 ); + + // conver to the manager + pMan = Abc_NtkToDar( pNtk ); + // derive CNF + pCnf = Cnf_Derive( pMan ); + // convert into the SAT solver + pSat = Cnf_DataWriteIntoSolver( pCnf ); + vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan ); + Aig_ManStop( pMan ); + Cnf_DataFree( pCnf ); + // solve SAT + if ( pSat == NULL ) + { + Vec_IntFree( vCiIds ); +// printf( "Trivially unsat\n" ); + return 1; + } + + +// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); + PRT( "Time", clock() - clk ); + + // simplify the problem + clk = clock(); + status = sat_solver_simplify(pSat); +// printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); +// PRT( "Time", clock() - clk ); + if ( status == 0 ) + { + Vec_IntFree( vCiIds ); + sat_solver_delete( pSat ); +// printf( "The problem is UNSATISFIABLE after simplification.\n" ); + return 1; + } + + // solve the miter + clk = clock(); + if ( fVerbose ) + pSat->verbosity = 1; + status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)nInsLimit, (sint64)0, (sint64)0 ); + if ( status == l_Undef ) + { +// printf( "The problem timed out.\n" ); + RetValue = -1; + } + else if ( status == l_True ) + { +// printf( "The problem is SATISFIABLE.\n" ); + RetValue = 0; + } + else if ( status == l_False ) + { +// printf( "The problem is UNSATISFIABLE.\n" ); + RetValue = 1; + } + else + assert( 0 ); +// PRT( "SAT sat_solver time", clock() - clk ); +// printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts ); + + // if the problem is SAT, get the counterexample + if ( status == l_True ) + { + pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); + } + // free the sat_solver + if ( fVerbose ) + Sat_SolverPrintStats( stdout, pSat ); +//sat_solver_store_write( pSat, "trace.cnf" ); +//sat_solver_store_free( pSat ); + sat_solver_delete( pSat ); + Vec_IntFree( vCiIds ); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c index 787e3f88..f0989b23 100644 --- a/src/base/abci/abcPart.c +++ b/src/base/abci/abcPart.c @@ -45,13 +45,17 @@ Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk ) Vec_Int_t * vSuppI; Abc_Obj_t * pObj, * pTemp; int i, k; + // set the PI numbers + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->pCopy = (void *)i; + // save hte CI numbers vSupports = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pObj, i ) { vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 ); vSuppI = (Vec_Int_t *)vSupp; Vec_PtrForEachEntry( vSupp, pTemp, k ) - Vec_IntWriteEntry( vSuppI, k, pTemp->Id ); + Vec_IntWriteEntry( vSuppI, k, (int)pTemp->pCopy ); Vec_IntSort( vSuppI, 0 ); // append the number of this output Vec_IntPush( vSuppI, i ); @@ -65,6 +69,71 @@ Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk ) /**Function************************************************************* + Synopsis [Start char-bases support representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_NtkSuppCharStart( Vec_Int_t * vOne, int nPis ) +{ + char * pBuffer; + int i, Entry; + pBuffer = ALLOC( char, nPis ); + memset( pBuffer, 0, sizeof(char) * nPis ); + Vec_IntForEachEntry( vOne, Entry, i ) + { + assert( Entry < nPis ); + pBuffer[Entry] = 1; + } + return pBuffer; +} + +/**Function************************************************************* + + Synopsis [Add to char-bases support representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkSuppCharAdd( char * pBuffer, Vec_Int_t * vOne, int nPis ) +{ + int i, Entry; + Vec_IntForEachEntry( vOne, Entry, i ) + { + assert( Entry < nPis ); + pBuffer[Entry] = 1; + } +} + +/**Function************************************************************* + + Synopsis [Find the common variables using char-bases support representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkSuppCharCommon( char * pBuffer, Vec_Int_t * vOne ) +{ + int i, Entry, nCommon = 0; + Vec_IntForEachEntry( vOne, Entry, i ) + nCommon += pBuffer[Entry]; + return nCommon; +} + +/**Function************************************************************* + Synopsis [Find the best partition.] Description [] @@ -74,8 +143,9 @@ Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vPartsAll, int nPartSizeLimit, Vec_Int_t * vOne ) +int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsChar, int nPartSizeLimit, Vec_Int_t * vOne ) { +/* Vec_Int_t * vPartSupp, * vPart; double Attract, Repulse, Cost, CostBest; int i, nCommon, iBest; @@ -83,12 +153,12 @@ int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vParts CostBest = 0.0; Vec_PtrForEachEntry( vPartSuppsAll, vPartSupp, i ) { + vPart = Vec_PtrEntry( vPartsAll, i ); + if ( nPartSizeLimit > 0 && Vec_IntSize(vPart) >= nPartSizeLimit ) + continue; nCommon = Vec_IntTwoCountCommon( vPartSupp, vOne ); if ( nCommon == 0 ) continue; - vPart = Vec_PtrEntry( vPartsAll, i ); - if ( nPartSizeLimit > 0 && Vec_IntSize(vPart) > nPartSizeLimit ) - continue; if ( nCommon == Vec_IntSize(vOne) ) return i; Attract = 1.0 * nCommon / Vec_IntSize(vOne); @@ -106,6 +176,41 @@ int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vParts if ( CostBest < 0.6 ) return -1; return iBest; +*/ + + Vec_Int_t * vPartSupp, * vPart; + int Attract, Repulse, Value, ValueBest; + int i, nCommon, iBest; +// int nCommon2; + iBest = -1; + ValueBest = 0; + Vec_PtrForEachEntry( vPartSuppsAll, vPartSupp, i ) + { + vPart = Vec_PtrEntry( vPartsAll, i ); + if ( nPartSizeLimit > 0 && Vec_IntSize(vPart) >= nPartSizeLimit ) + continue; +// nCommon2 = Vec_IntTwoCountCommon( vPartSupp, vOne ); + nCommon = Abc_NtkSuppCharCommon( Vec_PtrEntry(vPartSuppsChar, i), vOne ); +// assert( nCommon2 == nCommon ); + if ( nCommon == 0 ) + continue; + if ( nCommon == Vec_IntSize(vOne) ) + return i; + Attract = 1000 * nCommon / Vec_IntSize(vOne); + if ( Vec_IntSize(vPartSupp) < 100 ) + Repulse = 1; + else + Repulse = 1+Extra_Base2Log(Vec_IntSize(vPartSupp)-100); + Value = Attract/Repulse; + if ( ValueBest < Value ) + { + ValueBest = Value; + iBest = i; + } + } + if ( ValueBest < 75 ) + return -1; + return iBest; } /**Function************************************************************* @@ -222,9 +327,10 @@ void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll, ***********************************************************************/ Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose ) { + Vec_Ptr_t * vPartSuppsChar; Vec_Ptr_t * vSupps, * vPartsAll, * vPartsAll2, * vPartSuppsAll, * vPartPtr; Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp; - int i, iPart, iOut, clk; + int i, iPart, iOut, clk, clk2, timeFind = 0; // compute the supports for all outputs clk = clock(); @@ -233,6 +339,8 @@ if ( fVerbose ) { PRT( "Supps", clock() - clk ); } + // start char-based support representation + vPartSuppsChar = Vec_PtrAlloc( 1000 ); // create partitions clk = clock(); @@ -243,7 +351,10 @@ clk = clock(); // get the output number iOut = Vec_IntPop(vOne); // find closely matching part - iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vPartsAll, nPartSizeLimit, vOne ); +clk2 = clock(); + iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vPartsAll, vPartSuppsChar, nPartSizeLimit, vOne ); +timeFind += clock() - clk2; +//printf( "%4d->%4d ", i, iPart ); if ( iPart == -1 ) { // create new partition @@ -254,6 +365,8 @@ clk = clock(); // add this partition and its support Vec_PtrPush( vPartsAll, vPart ); Vec_PtrPush( vPartSuppsAll, vPartSupp ); + + Vec_PtrPush( vPartSuppsChar, Abc_NtkSuppCharStart(vOne, Abc_NtkPiNum(pNtk)) ); } else { @@ -266,11 +379,21 @@ clk = clock(); Vec_IntFree( vTemp ); // reinsert new support Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp ); + + Abc_NtkSuppCharAdd( Vec_PtrEntry(vPartSuppsChar, iPart), vOne, Abc_NtkPiNum(pNtk) ); } } + + // stop char-based support representation + Vec_PtrForEachEntry( vPartSuppsChar, vTemp, i ) + free( vTemp ); + Vec_PtrFree( vPartSuppsChar ); + +//printf( "\n" ); if ( fVerbose ) { PRT( "Parts", clock() - clk ); +//PRT( "Find ", timeFind ); } clk = clock(); @@ -290,7 +413,9 @@ clk = clock(); // Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll ); Abc_NtkPartitionCompact( vPartsAll, vPartSuppsAll, nPartSizeLimit ); if ( fVerbose ) - Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll ); +// Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll ); + printf( "Created %d partitions.\n", Vec_PtrSize(vPartsAll) ); + if ( fVerbose ) { PRT( "Comps", clock() - clk ); @@ -676,7 +801,7 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams ) // perform partitioning assert( Abc_NtkIsStrash(pNtk) ); // vParts = Abc_NtkPartitionNaive( pNtk, 20 ); - vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 ); + vParts = Abc_NtkPartitionSmart( pNtk, 0, 1 ); Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" ); diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c index cbbea1be..2376b72c 100644 --- a/src/base/abci/abcRewrite.c +++ b/src/base/abci/abcRewrite.c @@ -70,6 +70,13 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb // cleanup the AIG Abc_AigCleanup(pNtk->pManFunc); + { + Vec_Vec_t * vParts; + vParts = Abc_NtkPartitionSmart( pNtk, 50, 1 ); + Vec_VecFree( vParts ); + } + + // start placement package if ( fPlaceEnable ) { diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index d9cae254..aafa6530 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -49,7 +49,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int sat_solver * pSat; lbool status; int RetValue, clk; - + if ( pNumConfs ) *pNumConfs = 0; if ( pNumInspects ) @@ -70,7 +70,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int //return 1; // printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); -// PRT( "Time", clock() - clk ); + PRT( "Time", clock() - clk ); // simplify the problem clk = clock(); diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index b1a0dc5b..978b7cdb 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -351,7 +351,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, int fReco ***********************************************************************/ Abc_Obj_t * Abc_NtkTopmost_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int LevelCut ) { - assert( Abc_ObjIsComplement(pNode) ); + assert( !Abc_ObjIsComplement(pNode) ); if ( pNode->pCopy ) return pNode->pCopy; if ( pNode->Level <= (unsigned)LevelCut ) @@ -388,6 +388,7 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels ) // create PIs below the cut and nodes above the cut Abc_NtkCleanCopy( pNtk ); pObjNew = Abc_NtkTopmost_rec( pNtkNew, Abc_ObjFanin0(Abc_NtkPo(pNtk, 0)), LevelCut ); + pObjNew = Abc_ObjNotCond( pObjNew, Abc_ObjFaninC0(Abc_NtkPo(pNtk, 0)) ); // add the PO node and name pPoNew = Abc_NtkCreatePo(pNtkNew); Abc_ObjAddFanin( pPoNew, pObjNew ); diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c index 5d5e6e93..967e4617 100644 --- a/src/base/abci/abcTiming.c +++ b/src/base/abci/abcTiming.c @@ -819,6 +819,7 @@ void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ) { if ( !Abc_ObjIsCo(pFanout) && !pFanout->fMarkA ) { + assert( Abc_ObjLevel(pFanout) >= Lev ); Vec_VecPush( vLevels, Abc_ObjLevel(pFanout), pFanout ); pFanout->fMarkA = 1; } @@ -840,7 +841,7 @@ void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ) void Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ) { Abc_Obj_t * pFanin, * pTemp; - int LevelOld, Lev, k, m; + int LevelOld, LevFanin, Lev, k, m; // check if level has changed LevelOld = Abc_ObjReverseLevel(pObjNew); if ( LevelOld == Abc_ObjReverseLevelNew(pObjNew) ) @@ -866,7 +867,9 @@ void Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ) { if ( !Abc_ObjIsCi(pFanin) && !pFanin->fMarkA ) { - Vec_VecPush( vLevels, Abc_ObjReverseLevel(pFanin), pFanin ); + LevFanin = Abc_ObjReverseLevel( pFanin ); + assert( LevFanin >= Lev ); + Vec_VecPush( vLevels, LevFanin, pFanin ); pFanin->fMarkA = 1; } } @@ -891,6 +894,7 @@ void Abc_NtkUpdate( Abc_Obj_t * pObj, Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ) Abc_ObjReplace( pObj, pObjNew ); // update the level of the node Abc_NtkUpdateLevel( pObjNew, vLevels ); + Abc_ObjSetReverseLevel( pObjNew, 0 ); Abc_NtkUpdateReverseLevel( pObjNew, vLevels ); } diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 6ab2c552..63ba4843 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -368,7 +368,7 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" ); // partition the outputs - vParts = Abc_NtkPartitionSmart( pMiter, 50, 0 ); + vParts = Abc_NtkPartitionSmart( pMiter, 50, 1 ); // fraig each partition Status = 1; diff --git a/src/misc/extra/extraUtilProgress.c b/src/misc/extra/extraUtilProgress.c index 51095016..6b6d5132 100644 --- a/src/misc/extra/extraUtilProgress.c +++ b/src/misc/extra/extraUtilProgress.c @@ -68,7 +68,7 @@ ProgressBar * Extra_ProgressBarStart( FILE * pFile, int nItemsTotal ) p->nItemsTotal = nItemsTotal; p->posTotal = 78; p->posCur = 1; - p->nItemsNext = (int)((float)p->nItemsTotal/p->posTotal)*(p->posCur+5)+2; + p->nItemsNext = (int)((7.0+p->posCur)*p->nItemsTotal/p->posTotal); Extra_ProgressBarShow( p, NULL ); return p; } @@ -89,12 +89,16 @@ void Extra_ProgressBarUpdate_int( ProgressBar * p, int nItemsCur, char * pString if ( p == NULL ) return; if ( nItemsCur < p->nItemsNext ) return; - if ( nItemsCur > p->nItemsTotal ) - nItemsCur = p->nItemsTotal; - p->posCur = (int)((double)nItemsCur * p->posTotal / p->nItemsTotal); - p->nItemsNext = (int)((double)p->nItemsTotal/p->posTotal)*(p->posCur+10)+1; - if ( p->posCur == 0 ) - p->posCur = 1; + if ( nItemsCur >= p->nItemsTotal ) + { + p->posCur = 78; + p->nItemsNext = 0x7FFFFFFF; + } + else + { + p->posCur += 7; + p->nItemsNext = (int)((7.0+p->posCur)*p->nItemsTotal/p->posTotal); + } Extra_ProgressBarShow( p, pString ); } diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 5c4a5ab9..df6f824c 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -788,15 +788,19 @@ static inline void Vec_IntSortUnsigned( Vec_Int_t * p ) ***********************************************************************/ static inline int Vec_IntTwoCountCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2 ) { - int i, k, Counter = 0; - for ( i = k = 0; i < Vec_IntSize(vArr1) && k < Vec_IntSize(vArr2); ) + int * pBeg1 = vArr1->pArray; + int * pBeg2 = vArr2->pArray; + int * pEnd1 = vArr1->pArray + vArr1->nSize; + int * pEnd2 = vArr2->pArray + vArr2->nSize; + int Counter = 0; + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) { - if ( Vec_IntEntry(vArr1,i) == Vec_IntEntry(vArr2,k) ) - Counter++, i++, k++; - else if ( Vec_IntEntry(vArr1,i) < Vec_IntEntry(vArr2,k) ) - i++; - else - k++; + if ( *pBeg1 == *pBeg2 ) + *pBeg1++, pBeg2++, Counter++; + else if ( *pBeg1 < *pBeg2 ) + *pBeg1++; + else + *pBeg2++; } return Counter; } @@ -814,22 +818,29 @@ static inline int Vec_IntTwoCountCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2 ) ***********************************************************************/ static inline Vec_Int_t * Vec_IntTwoMerge( Vec_Int_t * vArr1, Vec_Int_t * vArr2 ) { - Vec_Int_t * vArr; - int i, k; - vArr = Vec_IntAlloc( Vec_IntSize(vArr1) ); - for ( i = k = 0; i < Vec_IntSize(vArr1) && k < Vec_IntSize(vArr2); ) + Vec_Int_t * vArr = Vec_IntAlloc( vArr1->nSize + vArr2->nSize ); + int * pBeg = vArr->pArray; + int * pBeg1 = vArr1->pArray; + int * pBeg2 = vArr2->pArray; + int * pEnd1 = vArr1->pArray + vArr1->nSize; + int * pEnd2 = vArr2->pArray + vArr2->nSize; + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) { - if ( Vec_IntEntry(vArr1,i) == Vec_IntEntry(vArr2,k) ) - Vec_IntPush( vArr, Vec_IntEntry(vArr1,i) ), i++, k++; - else if ( Vec_IntEntry(vArr1,i) < Vec_IntEntry(vArr2,k) ) - Vec_IntPush( vArr, Vec_IntEntry(vArr1,i) ), i++; - else - Vec_IntPush( vArr, Vec_IntEntry(vArr2,k) ), k++; + if ( *pBeg1 == *pBeg2 ) + *pBeg++ = *pBeg1++, pBeg2++; + else if ( *pBeg1 < *pBeg2 ) + *pBeg++ = *pBeg1++; + else + *pBeg++ = *pBeg2++; } - for ( ; i < Vec_IntSize(vArr1); i++ ) - Vec_IntPush( vArr, Vec_IntEntry(vArr1,i) ); - for ( ; k < Vec_IntSize(vArr2); k++ ) - Vec_IntPush( vArr, Vec_IntEntry(vArr2,k) ); + while ( pBeg1 < pEnd1 ) + *pBeg++ = *pBeg1++; + while ( pBeg2 < pEnd2 ) + *pBeg++ = *pBeg2++; + vArr->nSize = pBeg - vArr->pArray; + assert( vArr->nSize <= vArr->nCap ); + assert( vArr->nSize >= vArr1->nSize ); + assert( vArr->nSize >= vArr2->nSize ); return vArr; } diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 5c9294b0..512c5751 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1195,7 +1195,8 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin double Ratio = (s->stats.learnts == 0)? 0.0 : s->stats.learnts_literals / (double)s->stats.learnts; - if (s->verbosity >= 1){ + if (s->verbosity >= 1) + { printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", (double)s->stats.conflicts, (double)s->stats.clauses, |