| /**CFile**************************************************************** |
| |
| FileName [covMinSop.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Mapping into network of SOPs/ESOPs.] |
| |
| Synopsis [SOP manipulation.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: covMinSop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "covInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| static void Min_SopRewrite( Min_Man_t * p ); |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Min_SopMinimize( Min_Man_t * p ) |
| { |
| int nCubesInit, nCubesOld, nIter; |
| if ( p->nCubes < 3 ) |
| return; |
| nIter = 0; |
| nCubesInit = p->nCubes; |
| do { |
| nCubesOld = p->nCubes; |
| Min_SopRewrite( p ); |
| nIter++; |
| // printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes ); |
| } |
| while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 ); |
| // printf( "\n" ); |
| |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Min_SopRewrite( Min_Man_t * p ) |
| { |
| Min_Cube_t * pCube, ** ppPrev; |
| Min_Cube_t * pThis, ** ppPrevT; |
| Min_Cube_t * pTemp; |
| int v00, v01, v10, v11, Var0, Var1, Index, fCont0, fCont1, nCubesOld; |
| int nPairs = 0; |
| /* |
| { |
| Min_Cube_t * pCover; |
| pCover = Min_CoverCollect( p, p->nVars ); |
| printf( "\n\n" ); |
| Min_CoverWrite( stdout, pCover ); |
| Min_CoverExpand( p, pCover ); |
| } |
| */ |
| |
| // insert the bubble before the first cube |
| p->pBubble->pNext = p->ppStore[0]; |
| p->ppStore[0] = p->pBubble; |
| p->pBubble->nLits = 0; |
| |
| // go through the cubes |
| while ( 1 ) |
| { |
| // get the index of the bubble |
| Index = p->pBubble->nLits; |
| |
| // find the bubble |
| Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev ) |
| if ( pCube == p->pBubble ) |
| break; |
| assert( pCube == p->pBubble ); |
| |
| // remove the bubble, get the next cube after the bubble |
| *ppPrev = p->pBubble->pNext; |
| pCube = p->pBubble->pNext; |
| if ( pCube == NULL ) |
| for ( Index++; Index <= p->nVars; Index++ ) |
| if ( p->ppStore[Index] ) |
| { |
| ppPrev = &(p->ppStore[Index]); |
| pCube = p->ppStore[Index]; |
| break; |
| } |
| // stop if there is no more cubes |
| if ( pCube == NULL ) |
| break; |
| |
| // find the first dist2 cube |
| Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT ) |
| if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) |
| break; |
| if ( pThis == NULL && Index < p->nVars ) |
| Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT ) |
| if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) |
| break; |
| // continue if there is no dist2 cube |
| if ( pThis == NULL ) |
| { |
| // insert the bubble after the cube |
| p->pBubble->pNext = pCube->pNext; |
| pCube->pNext = p->pBubble; |
| p->pBubble->nLits = pCube->nLits; |
| continue; |
| } |
| nPairs++; |
| /* |
| printf( "\n" ); |
| Min_CubeWrite( stdout, pCube ); |
| Min_CubeWrite( stdout, pThis ); |
| */ |
| // remove the cubes, insert the bubble instead of pCube |
| *ppPrevT = pThis->pNext; |
| *ppPrev = p->pBubble; |
| p->pBubble->pNext = pCube->pNext; |
| p->pBubble->nLits = pCube->nLits; |
| p->nCubes -= 2; |
| |
| assert( pCube != p->pBubble && pThis != p->pBubble ); |
| |
| |
| // save the dist2 parameters |
| v00 = Min_CubeGetVar( pCube, Var0 ); |
| v01 = Min_CubeGetVar( pCube, Var1 ); |
| v10 = Min_CubeGetVar( pThis, Var0 ); |
| v11 = Min_CubeGetVar( pThis, Var1 ); |
| assert( v00 != v10 && v01 != v11 ); |
| assert( v00 != 3 || v01 != 3 ); |
| assert( v10 != 3 || v11 != 3 ); |
| |
| //printf( "\n" ); |
| //Min_CubeWrite( stdout, pCube ); |
| //Min_CubeWrite( stdout, pThis ); |
| |
| //printf( "\n" ); |
| //Min_CubeWrite( stdout, pCube ); |
| //Min_CubeWrite( stdout, pThis ); |
| |
| // consider the case when both cubes have non-empty literals |
| if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 ) |
| { |
| assert( v00 == (v10 ^ 3) ); |
| assert( v01 == (v11 ^ 3) ); |
| // create the temporary cube equal to the first corner |
| Min_CubeXorVar( pCube, Var0, 3 ); |
| // check if this cube is contained |
| fCont0 = Min_CoverContainsCube( p, pCube ); |
| // create the temporary cube equal to the first corner |
| Min_CubeXorVar( pCube, Var0, 3 ); |
| Min_CubeXorVar( pCube, Var1, 3 ); |
| //printf( "\n" ); |
| //Min_CubeWrite( stdout, pCube ); |
| //Min_CubeWrite( stdout, pThis ); |
| // check if this cube is contained |
| fCont1 = Min_CoverContainsCube( p, pCube ); |
| // undo the change |
| Min_CubeXorVar( pCube, Var1, 3 ); |
| |
| // check if the cubes can be overwritten |
| if ( fCont0 && fCont1 ) |
| { |
| // one of the cubes can be recycled, the other expanded and added |
| Min_CubeRecycle( p, pThis ); |
| // remove the literals |
| Min_CubeXorVar( pCube, Var0, v00 ^ 3 ); |
| Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); |
| pCube->nLits -= 2; |
| Min_SopAddCube( p, pCube ); |
| } |
| else if ( fCont0 ) |
| { |
| // expand both cubes and add them |
| Min_CubeXorVar( pCube, Var0, v00 ^ 3 ); |
| pCube->nLits--; |
| Min_SopAddCube( p, pCube ); |
| Min_CubeXorVar( pThis, Var1, v11 ^ 3 ); |
| pThis->nLits--; |
| Min_SopAddCube( p, pThis ); |
| } |
| else if ( fCont1 ) |
| { |
| // expand both cubes and add them |
| Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); |
| pCube->nLits--; |
| Min_SopAddCube( p, pCube ); |
| Min_CubeXorVar( pThis, Var0, v10 ^ 3 ); |
| pThis->nLits--; |
| Min_SopAddCube( p, pThis ); |
| } |
| else |
| { |
| Min_SopAddCube( p, pCube ); |
| Min_SopAddCube( p, pThis ); |
| } |
| // otherwise, no change is possible |
| continue; |
| } |
| |
| // if one of them does not have DC lit, move it |
| if ( v00 != 3 && v01 != 3 ) |
| { |
| assert( v10 == 3 || v11 == 3 ); |
| pTemp = pCube; pCube = pThis; pThis = pTemp; |
| Index = v00; v00 = v10; v10 = Index; |
| Index = v01; v01 = v11; v11 = Index; |
| } |
| |
| // make sure the first cube has first var DC |
| if ( v00 != 3 ) |
| { |
| assert( v01 == 3 ); |
| Index = Var0; Var0 = Var1; Var1 = Index; |
| Index = v00; v00 = v01; v01 = Index; |
| Index = v10; v10 = v11; v11 = Index; |
| } |
| |
| // consider both cases: both have DC lit |
| if ( v00 == 3 && v11 == 3 ) |
| { |
| assert( v01 != 3 && v10 != 3 ); |
| // try the remaining minterm |
| // create the temporary cube equal to the first corner |
| Min_CubeXorVar( pCube, Var0, v10 ); |
| Min_CubeXorVar( pCube, Var1, 3 ); |
| pCube->nLits++; |
| // check if this cube is contained |
| fCont0 = Min_CoverContainsCube( p, pCube ); |
| // undo the cube transformations |
| Min_CubeXorVar( pCube, Var0, v10 ); |
| Min_CubeXorVar( pCube, Var1, 3 ); |
| pCube->nLits--; |
| // check the case when both are covered |
| if ( fCont0 ) |
| { |
| // one of the cubes can be recycled, the other expanded and added |
| Min_CubeRecycle( p, pThis ); |
| // remove the literals |
| Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); |
| pCube->nLits--; |
| Min_SopAddCube( p, pCube ); |
| } |
| else |
| { |
| // try two reduced cubes |
| Min_CubeXorVar( pCube, Var0, v10 ); |
| pCube->nLits++; |
| // remember the cubes |
| nCubesOld = p->nCubes; |
| Min_SopAddCube( p, pCube ); |
| // check if the cube is absorbed |
| if ( p->nCubes < nCubesOld + 1 ) |
| { // absorbed - add the second cube |
| Min_SopAddCube( p, pThis ); |
| } |
| else |
| { // remove this cube, and try another one |
| assert( pCube == p->ppStore[pCube->nLits] ); |
| p->ppStore[pCube->nLits] = pCube->pNext; |
| p->nCubes--; |
| |
| // return the cube to the previous state |
| Min_CubeXorVar( pCube, Var0, v10 ); |
| pCube->nLits--; |
| |
| // generate another reduced cube |
| Min_CubeXorVar( pThis, Var1, v01 ); |
| pThis->nLits++; |
| |
| // add both cubes |
| Min_SopAddCube( p, pCube ); |
| Min_SopAddCube( p, pThis ); |
| } |
| } |
| } |
| else // the first cube has DC lit |
| { |
| assert( v01 != 3 && v10 != 3 && v11 != 3 ); |
| // try the remaining minterm |
| // create the temporary cube equal to the minterm |
| Min_CubeXorVar( pThis, Var0, 3 ); |
| // check if this cube is contained |
| fCont0 = Min_CoverContainsCube( p, pThis ); |
| // undo the cube transformations |
| Min_CubeXorVar( pThis, Var0, 3 ); |
| // check the case when both are covered |
| if ( fCont0 ) |
| { |
| // one of the cubes can be recycled, the other expanded and added |
| Min_CubeRecycle( p, pThis ); |
| // remove the literals |
| Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); |
| pCube->nLits--; |
| Min_SopAddCube( p, pCube ); |
| } |
| else |
| { |
| // try reshaping the cubes |
| // reduce the first cube |
| Min_CubeXorVar( pCube, Var0, v10 ); |
| pCube->nLits++; |
| // expand the second cube |
| Min_CubeXorVar( pThis, Var1, v11 ^ 3 ); |
| pThis->nLits--; |
| // add both cubes |
| Min_SopAddCube( p, pCube ); |
| Min_SopAddCube( p, pThis ); |
| } |
| } |
| } |
| // printf( "Pairs = %d ", nPairs ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Adds cube to the SOP cover stored in the manager.] |
| |
| Description [Returns 0 if the cube is added or removed. Returns 1 |
| if the cube is glued with some other cube and has to be added again.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Min_SopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube ) |
| { |
| Min_Cube_t * pThis, * pThis2, ** ppPrev; |
| int i; |
| // try to find the identical cube |
| Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) |
| { |
| if ( Min_CubesAreEqual( pCube, pThis ) ) |
| { |
| Min_CubeRecycle( p, pCube ); |
| return 0; |
| } |
| } |
| // try to find a containing cube |
| for ( i = 0; i < (int)pCube->nLits; i++ ) |
| Min_CoverForEachCube( p->ppStore[i], pThis ) |
| { |
| if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) ) |
| { |
| Min_CubeRecycle( p, pCube ); |
| return 0; |
| } |
| } |
| // try to find distance one in the same bin |
| Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev ) |
| { |
| if ( Min_CubesDistOne( pCube, pThis, NULL ) ) |
| { |
| *ppPrev = pThis->pNext; |
| Min_CubesTransformOr( pCube, pThis ); |
| pCube->nLits--; |
| Min_CubeRecycle( p, pThis ); |
| p->nCubes--; |
| return 1; |
| } |
| } |
| |
| // clean the other cubes using this one |
| for ( i = pCube->nLits + 1; i <= (int)pCube->nVars; i++ ) |
| { |
| ppPrev = &p->ppStore[i]; |
| Min_CoverForEachCubeSafe( p->ppStore[i], pThis, pThis2 ) |
| { |
| if ( pThis != p->pBubble && Min_CubeIsContained( pCube, pThis ) ) |
| { |
| *ppPrev = pThis->pNext; |
| Min_CubeRecycle( p, pThis ); |
| p->nCubes--; |
| } |
| else |
| ppPrev = &pThis->pNext; |
| } |
| } |
| |
| // add the cube |
| pCube->pNext = p->ppStore[pCube->nLits]; |
| p->ppStore[pCube->nLits] = pCube; |
| p->nCubes++; |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Adds the cube to storage.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) |
| { |
| assert( Min_CubeCheck( pCube ) ); |
| assert( pCube != p->pBubble ); |
| assert( (int)pCube->nLits == Min_CubeCountLits(pCube) ); |
| while ( Min_SopAddCubeInt( p, pCube ) ); |
| } |
| |
| |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Min_SopContain( Min_Man_t * p ) |
| { |
| Min_Cube_t * pCube, * pCube2, ** ppPrev; |
| int i, k; |
| for ( i = 0; i <= p->nVars; i++ ) |
| { |
| Min_CoverForEachCube( p->ppStore[i], pCube ) |
| Min_CoverForEachCubePrev( pCube->pNext, pCube2, ppPrev ) |
| { |
| if ( !Min_CubesAreEqual( pCube, pCube2 ) ) |
| continue; |
| *ppPrev = pCube2->pNext; |
| Min_CubeRecycle( p, pCube2 ); |
| p->nCubes--; |
| } |
| for ( k = i + 1; k <= p->nVars; k++ ) |
| Min_CoverForEachCubePrev( p->ppStore[k], pCube2, ppPrev ) |
| { |
| if ( !Min_CubeIsContained( pCube, pCube2 ) ) |
| continue; |
| *ppPrev = pCube2->pNext; |
| Min_CubeRecycle( p, pCube2 ); |
| p->nCubes--; |
| } |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Min_SopDist1Merge( Min_Man_t * p ) |
| { |
| Min_Cube_t * pCube, * pCube2, * pCubeNew; |
| int i; |
| for ( i = p->nVars; i >= 0; i-- ) |
| { |
| Min_CoverForEachCube( p->ppStore[i], pCube ) |
| Min_CoverForEachCube( pCube->pNext, pCube2 ) |
| { |
| assert( pCube->nLits == pCube2->nLits ); |
| if ( !Min_CubesDistOne( pCube, pCube2, NULL ) ) |
| continue; |
| pCubeNew = Min_CubesXor( p, pCube, pCube2 ); |
| assert( pCubeNew->nLits == pCube->nLits - 1 ); |
| pCubeNew->pNext = p->ppStore[pCubeNew->nLits]; |
| p->ppStore[pCubeNew->nLits] = pCubeNew; |
| p->nCubes++; |
| } |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp ) |
| { |
| Vec_Int_t * vVars; |
| Min_Cube_t * pCover, * pCube, * pNext, * pReady, * pThis, ** ppPrev; |
| int Num, Value, i; |
| |
| // get the variables |
| vVars = Vec_IntAlloc( 100 ); |
| // create the tautology cube |
| pCover = Min_CubeAlloc( p ); |
| // sharp it with all cubes |
| Min_CoverForEachCube( pSharp, pCube ) |
| Min_CoverForEachCubePrev( pCover, pThis, ppPrev ) |
| { |
| if ( Min_CubesDisjoint( pThis, pCube ) ) |
| continue; |
| // remember the next pointer |
| pNext = pThis->pNext; |
| // get the variables, in which pThis is '-' while pCube is fixed |
| Min_CoverGetDisjVars( pThis, pCube, vVars ); |
| // generate the disjoint cubes |
| pReady = pThis; |
| Vec_IntForEachEntryReverse( vVars, Num, i ) |
| { |
| // correct the literal |
| Min_CubeXorVar( pReady, vVars->pArray[i], 3 ); |
| if ( i == 0 ) |
| break; |
| // create the new cube and clean this value |
| Value = Min_CubeGetVar( pReady, vVars->pArray[i] ); |
| pReady = Min_CubeDup( p, pReady ); |
| Min_CubeXorVar( pReady, vVars->pArray[i], 3 ^ Value ); |
| // add to the cover |
| *ppPrev = pReady; |
| ppPrev = &pReady->pNext; |
| } |
| pThis = pReady; |
| pThis->pNext = pNext; |
| } |
| Vec_IntFree( vVars ); |
| |
| // perform dist-1 merge and contain |
| Min_CoverExpandRemoveEqual( p, pCover ); |
| Min_SopDist1Merge( p ); |
| Min_SopContain( p ); |
| return Min_CoverCollect( p, p->nVars ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Min_SopCheck( Min_Man_t * p ) |
| { |
| Min_Cube_t * pCube, * pThis; |
| int i; |
| |
| pCube = Min_CubeAlloc( p ); |
| Min_CubeXorBit( pCube, 2*0+1 ); |
| Min_CubeXorBit( pCube, 2*1+1 ); |
| Min_CubeXorBit( pCube, 2*2+0 ); |
| Min_CubeXorBit( pCube, 2*3+0 ); |
| Min_CubeXorBit( pCube, 2*4+0 ); |
| Min_CubeXorBit( pCube, 2*5+1 ); |
| Min_CubeXorBit( pCube, 2*6+1 ); |
| pCube->nLits = 7; |
| |
| // Min_CubeWrite( stdout, pCube ); |
| |
| // check that the cubes contain it |
| for ( i = 0; i <= p->nVars; i++ ) |
| Min_CoverForEachCube( p->ppStore[i], pThis ) |
| if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) ) |
| { |
| Min_CubeRecycle( p, pCube ); |
| return 1; |
| } |
| Min_CubeRecycle( p, pCube ); |
| return 0; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
