From de695c9d4c5fbc0e48e30d8aeefd8fe1f9a51507 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 12 Jan 2016 11:55:50 -0800 Subject: Better print-out of SOPs. Changing default of 'fx'. Updating 'satclp' to fine prine SOPs. --- src/base/abc/abc.h | 1 + src/base/abc/abcFanOrder.c | 187 ++++++++++++++++++++++++++++++++++++++++++-- src/base/abc/abcFunc.c | 1 - src/base/abci/abcCollapse.c | 3 +- src/base/abci/abcFxu.c | 2 +- 5 files changed, 184 insertions(+), 10 deletions(-) (limited to 'src') diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 23da283d..3098f1d1 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -653,6 +653,7 @@ extern ABC_DLL void Abc_ObjReplace( Abc_Obj_t * pObjOld, Abc_Obj_t extern ABC_DLL int Abc_ObjFanoutFaninNum( Abc_Obj_t * pFanout, Abc_Obj_t * pFanin ); /*=== abcFanOrder.c ==========================================================*/ extern ABC_DLL int Abc_NtkMakeLegit( Abc_Ntk_t * pNtk ); +extern ABC_DLL void Abc_NtkSortSops( Abc_Ntk_t * pNtk ); /*=== abcFraig.c ==========================================================*/ extern ABC_DLL Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc ); extern ABC_DLL void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc ); diff --git a/src/base/abc/abcFanOrder.c b/src/base/abc/abcFanOrder.c index 31b710c2..bfd99f38 100644 --- a/src/base/abc/abcFanOrder.c +++ b/src/base/abc/abcFanOrder.c @@ -31,6 +31,7 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// + /**Function************************************************************* Synopsis [Reorder fanins of the network.] @@ -87,12 +88,153 @@ void Abc_NtkOrderFaninsById( Abc_Ntk_t * pNtk ) Vec_IntFree( vOrder ); Vec_StrFree( vStore ); } + +/**Function************************************************************* + + Synopsis [Returns fanin permutation to reorders columns lexicographically.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkSopTranspose( char * pSop, int nVars, Vec_Ptr_t * vCubes, Vec_Str_t * vStore ) +{ + char * pCube; + int nCubes, v, c; + // collect original cubes + Vec_PtrClear( vCubes ); + Abc_SopForEachCube( pSop, nVars, pCube ) + Vec_PtrPush( vCubes, pCube ); + // rebuild the cubes + Vec_StrClear( vStore ); + for ( v = 0; v < nVars; v++ ) + { + Vec_PtrForEachEntry( char *, vCubes, pCube, c ) + Vec_StrPush( vStore, pCube[v] ); + Vec_StrPush( vStore, '\0' ); + } + // get the cubes + nCubes = Vec_PtrSize( vCubes ); + Vec_PtrClear( vCubes ); + for ( v = 0; v < nVars; v++ ) + Vec_PtrPush( vCubes, Vec_StrEntryP(vStore, v*(nCubes+1)) ); +} +static inline void Vec_StrSelectSortCost( char ** pArray, int nSize, Vec_Int_t * vPerm ) +{ + int i, j, best_i, * pPerm; + Vec_IntClear( vPerm ); + for ( i = 0; i < nSize; i++ ) + Vec_IntPush( vPerm, i ); + pPerm = Vec_IntArray( vPerm ); + for ( i = 0; i < nSize-1; i++ ) + { + best_i = i; + for ( j = i+1; j < nSize; j++ ) + if ( strcmp(pArray[j], pArray[best_i]) < 0 ) + best_i = j; + ABC_SWAP( char *, pArray[i], pArray[best_i] ); + ABC_SWAP( int, pPerm[i], pPerm[best_i] ); + } +} +void Abc_NtkOrderFaninsBySortingColumns( Abc_Ntk_t * pNtk ) +{ + Vec_Int_t * vOrder; + Vec_Int_t * vCounts; + Vec_Int_t * vFanins; + Vec_Str_t * vStore; + Vec_Ptr_t * vCubes; + Abc_Obj_t * pNode; + char * pSop, * pSopNew; + char * pCube, * pCubeNew; + int nVars, i, v, * pOrder; + assert( Abc_NtkHasSop(pNtk) ); + vOrder = Vec_IntAlloc( 100 ); + vStore = Vec_StrAlloc( 100 ); + vCubes = Vec_PtrAlloc( 100 ); + vCounts = Vec_IntAlloc( 100 ); + vFanins = Vec_IntAlloc( 100 ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + pSop = (char *)pNode->pData; + nVars = Abc_SopGetVarNum(pSop); + assert( nVars == Abc_ObjFaninNum(pNode) ); + // create a transposed SOP + Abc_NtkSopTranspose( pSop, nVars, vCubes, vStore ); + // create permutation + Vec_StrSelectSortCost( (char **)Vec_PtrArray(vCubes), nVars, vOrder ); + pOrder = Vec_IntArray(vOrder); + // copy the cover + Vec_StrGrow( vStore, Abc_SopGetCubeNum(pSop) * (nVars + 3) + 1 ); + memcpy( Vec_StrArray(vStore), pSop, Abc_SopGetCubeNum(pSop) * (nVars + 3) + 1 ); + pSopNew = pCubeNew = pSop; + pSop = Vec_StrArray(vStore); + // generate permuted one + Abc_SopForEachCube( pSop, nVars, pCube ) + { + for ( v = 0; v < nVars; v++ ) + pCubeNew[v] = '-'; + for ( v = 0; v < nVars; v++ ) + if ( pCube[pOrder[v]] == '0' ) + pCubeNew[v] = '0'; + else if ( pCube[pOrder[v]] == '1' ) + pCubeNew[v] = '1'; + pCubeNew += nVars + 3; + } + pNode->pData = pSopNew; + // generate the fanin order + Vec_IntClear( vFanins ); + for ( v = 0; v < nVars; v++ ) + Vec_IntPush( vFanins, Abc_ObjFaninId( pNode, pOrder[v] ) ); + Vec_IntClear( &pNode->vFanins ); + Vec_IntAppend( &pNode->vFanins, vFanins ); + } + Vec_IntFree( vFanins ); + Vec_IntFree( vCounts ); + Vec_IntFree( vOrder ); + Vec_StrFree( vStore ); + Vec_PtrFree( vCubes ); +} + + +/**Function************************************************************* + + Synopsis [Reorders columns by literal and then lexicographically.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_StrSelectSortCost2( char ** pArray, int nSize, Vec_Int_t * vCounts, Vec_Int_t * vPerm ) +{ + int i, j, best_i, * pPerm; + Vec_IntClear( vPerm ); + for ( i = 0; i < nSize; i++ ) + Vec_IntPush( vPerm, i ); + pPerm = Vec_IntArray( vPerm ); + for ( i = 0; i < nSize-1; i++ ) + { + best_i = i; + for ( j = i+1; j < nSize; j++ ) + if ( Vec_IntEntry(vCounts, pPerm[j]) < Vec_IntEntry(vCounts, pPerm[best_i]) || + (Vec_IntEntry(vCounts, pPerm[j]) == Vec_IntEntry(vCounts, pPerm[best_i]) && strcmp(pArray[j], pArray[best_i]) < 0) ) + best_i = j; + ABC_SWAP( char *, pArray[i], pArray[best_i] ); + ABC_SWAP( int, pPerm[i], pPerm[best_i] ); + } +} void Abc_NtkOrderFaninsByLitCount( Abc_Ntk_t * pNtk ) { Vec_Int_t * vOrder; Vec_Int_t * vCounts; Vec_Int_t * vFanins; Vec_Str_t * vStore; + Vec_Ptr_t * vCubes; Abc_Obj_t * pNode; char * pSop, * pSopNew; char * pCube, * pCubeNew; @@ -100,6 +242,7 @@ void Abc_NtkOrderFaninsByLitCount( Abc_Ntk_t * pNtk ) assert( Abc_NtkHasSop(pNtk) ); vOrder = Vec_IntAlloc( 100 ); vStore = Vec_StrAlloc( 100 ); + vCubes = Vec_PtrAlloc( 100 ); vCounts = Vec_IntAlloc( 100 ); vFanins = Vec_IntAlloc( 100 ); Abc_NtkForEachNode( pNtk, pNode, i ) @@ -113,12 +256,20 @@ void Abc_NtkOrderFaninsByLitCount( Abc_Ntk_t * pNtk ) for ( v = 0; v < nVars; v++ ) if ( pCube[v] != '-' ) Vec_IntAddToEntry( vCounts, v, 1 ); + + // create a transposed SOP + Abc_NtkSopTranspose( pSop, nVars, vCubes, vStore ); + // create permutation + Vec_StrSelectSortCost2( (char **)Vec_PtrArray(vCubes), nVars, vCounts, vOrder ); + pOrder = Vec_IntArray(vOrder); +/* // find good order Vec_IntClear( vOrder ); for ( v = 0; v < nVars; v++ ) Vec_IntPush( vOrder, v ); pOrder = Vec_IntArray(vOrder); Vec_IntSelectSortCost( pOrder, nVars, vCounts ); +*/ // copy the cover Vec_StrGrow( vStore, Abc_SopGetCubeNum(pSop) * (nVars + 3) + 1 ); memcpy( Vec_StrArray(vStore), pSop, Abc_SopGetCubeNum(pSop) * (nVars + 3) + 1 ); @@ -148,6 +299,7 @@ void Abc_NtkOrderFaninsByLitCount( Abc_Ntk_t * pNtk ) Vec_IntFree( vCounts ); Vec_IntFree( vOrder ); Vec_StrFree( vStore ); + Vec_PtrFree( vCubes ); } void Abc_NtkOrderFaninsByLitCountAndCubeCount( Abc_Ntk_t * pNtk ) { @@ -291,11 +443,27 @@ void Abc_NtkSplitLarge( Abc_Ntk_t * pNtk, int nFaninsMax, int nCubesMax ) SeeAlso [] ***********************************************************************/ -int Abc_NodeCompareCubes( char ** pp1, char ** pp2 ) +int Abc_NodeCompareCubes1( char ** pp1, char ** pp2 ) { return strcmp( *pp1, *pp2 ); } -void Abc_NodeSortCubes( Abc_Obj_t * pNode, Vec_Ptr_t * vCubes, Vec_Str_t * vStore ) +int Abc_NodeCompareCubes2( char ** pp1, char ** pp2 ) +{ + char * pStr1 = *pp1; + char * pStr2 = *pp2; + int i, nNum1 = 0, nNum2 = 0; + for ( i = 0; pStr1[i]; i++ ) + { + nNum1 += (pStr1[i] != '-'); + nNum2 += (pStr2[i] != '-'); + } + if ( nNum1 > nNum2 ) + return -1; + if ( nNum1 < nNum2 ) + return 1; + return strcmp( *pp1, *pp2 ); +} +void Abc_NodeSortCubes( Abc_Obj_t * pNode, Vec_Ptr_t * vCubes, Vec_Str_t * vStore, int fWeight ) { char * pCube, * pPivot; char * pSop = (char *)pNode->pData; @@ -307,7 +475,10 @@ void Abc_NodeSortCubes( Abc_Obj_t * pNode, Vec_Ptr_t * vCubes, Vec_Str_t * vStor pCube[nVars] = 0; Vec_PtrPush( vCubes, pCube ); } - Vec_PtrSort( vCubes, (int (*)())Abc_NodeCompareCubes ); + if ( fWeight ) + Vec_PtrSort( vCubes, (int (*)())Abc_NodeCompareCubes2 ); + else + Vec_PtrSort( vCubes, (int (*)())Abc_NodeCompareCubes1 ); Vec_StrGrow( vStore, Vec_PtrSize(vCubes) * (nVars + 3) ); pPivot = Vec_StrArray( vStore ); Vec_PtrForEachEntry( char *, vCubes, pCube, i ) @@ -319,7 +490,7 @@ void Abc_NodeSortCubes( Abc_Obj_t * pNode, Vec_Ptr_t * vCubes, Vec_Str_t * vStor } memcpy( pSop, Vec_StrArray(vStore), Vec_PtrSize(vCubes) * (nVars + 3) ); } -void Abc_NtkSortCubes( Abc_Ntk_t * pNtk ) +void Abc_NtkSortCubes( Abc_Ntk_t * pNtk, int fWeight ) { Vec_Ptr_t * vCubes; Vec_Str_t * vStore; @@ -329,11 +500,12 @@ void Abc_NtkSortCubes( Abc_Ntk_t * pNtk ) vCubes = Vec_PtrAlloc( 1000 ); vStore = Vec_StrAlloc( 1000 ); Abc_NtkForEachNode( pNtk, pNode, i ) - Abc_NodeSortCubes( pNode, vCubes, vStore ); + Abc_NodeSortCubes( pNode, vCubes, vStore, fWeight ); Vec_StrFree( vStore ); Vec_PtrFree( vCubes ); } + /**Function************************************************************* Synopsis [Sorts fanins of each node to make SOPs more readable.] @@ -347,10 +519,11 @@ void Abc_NtkSortCubes( Abc_Ntk_t * pNtk ) ***********************************************************************/ void Abc_NtkSortSops( Abc_Ntk_t * pNtk ) { + Abc_NtkSortCubes( pNtk, 1 ); Abc_NtkOrderFaninsByLitCount( pNtk ); - Abc_NtkSortCubes( pNtk ); + Abc_NtkSortCubes( pNtk, 0 ); Abc_NtkOrderFaninsByLitCountAndCubeCount( pNtk ); - Abc_NtkSortCubes( pNtk ); + Abc_NtkSortCubes( pNtk, 0 ); } /**Function************************************************************* diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index 9799ee93..6b73bdc5 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -358,7 +358,6 @@ char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn, ***********************************************************************/ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fMode, int nCubeLimit ) { - extern void Abc_NtkSortSops( Abc_Ntk_t * pNtk ); Vec_Int_t * vGuide; Vec_Str_t * vCube; Abc_Obj_t * pNode; diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index 26574dee..6a132518 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -922,12 +922,13 @@ Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, in vSupp = Vec_WecEntry( vSupps, i ); Vec_IntForEachEntry( vSupp, iCi, k ) Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) ); - pNodeNew->pData = Vec_PtrEntry( vSops, i ); + pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Vec_PtrEntry( vSops, i ) ); assert( pNodeNew->pData != (void *)(ABC_PTRINT_T)1 ); Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); } Vec_WecFree( vSupps ); Vec_PtrFree( vSops ); + Abc_NtkSortSops( pNtkNew ); return pNtkNew; } Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose ) diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c index d2221f4e..8da306bf 100644 --- a/src/base/abci/abcFxu.c +++ b/src/base/abci/abcFxu.c @@ -56,7 +56,7 @@ void Abc_NtkSetDefaultFxParams( Fxu_Data_t * p ) p->nPairsMax = 30000; p->nNodesExt =1000000; p->WeightMin = 0; - p->LitCountMax= 0; + p->LitCountMax= 4; p->fOnlyS = 0; p->fOnlyD = 0; p->fUse0 = 0; -- cgit v1.2.3