From 23fd11037a006089898cb13494305e402a11ec76 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 29 Mar 2009 08:01:00 -0700 Subject: Version abc90329 --- src/map/cov/covMinSop.c | 615 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 615 insertions(+) create mode 100644 src/map/cov/covMinSop.c (limited to 'src/map/cov/covMinSop.c') diff --git a/src/map/cov/covMinSop.c b/src/map/cov/covMinSop.c new file mode 100644 index 00000000..731a6698 --- /dev/null +++ b/src/map/cov/covMinSop.c @@ -0,0 +1,615 @@ +/**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" + +//////////////////////////////////////////////////////////////////////// +/// 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 /// +//////////////////////////////////////////////////////////////////////// + + -- cgit v1.2.3