/**CFile****************************************************************
FileName [covMinEsop.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Mapping into network of SOPs/ESOPs.]
Synopsis [ESOP manipulation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: covMinEsop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "covInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Min_EsopRewrite( Min_Man_t * p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_EsopMinimize( Min_Man_t * p )
{
int nCubesInit, nCubesOld, nIter;
if ( p->nCubes < 3 )
return;
nIter = 0;
nCubesInit = p->nCubes;
do {
nCubesOld = p->nCubes;
Min_EsopRewrite( p );
nIter++;
}
while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
}
/**Function*************************************************************
Synopsis [Performs one round of rewriting using distance 2 cubes.]
Description [The weakness of this procedure is that it tries each cube
with only one distance-2 cube. If this pair does not lead to improvement
the cube is inserted into the cover anyhow, and we try another pair.
A possible improvement would be to try this cube with all distance-2
cubes, until an improvement is found, or until all such cubes are tried.]
SideEffects []
SeeAlso []
***********************************************************************/
void Min_EsopRewrite( Min_Man_t * p )
{
Min_Cube_t * pCube, ** ppPrev;
Min_Cube_t * pThis, ** ppPrevT;
int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld;
int nPairs = 0;
// 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;
if ( pThis == NULL && Index < p->nVars - 1 )
Min_CoverForEachCubePrev( p->ppStore[Index+2], 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++;
// 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;
// Exorlink-2:
// A{v00} B{v01} + A{v10} B{v11} =
// A{v00+v10} B{v01} + A{v10} B{v01+v11} =
// A{v00} B{v01+v11} + A{v00+v10} B{v11}
// save the dist2 parameters
v00 = Min_CubeGetVar( pCube, Var0 );
v01 = Min_CubeGetVar( pCube, Var1 );
v10 = Min_CubeGetVar( pThis, Var0 );
v11 = Min_CubeGetVar( pThis, Var1 );
//printf( "\n" );
//Min_CubeWrite( stdout, pCube );
//Min_CubeWrite( stdout, pThis );
// derive the first pair of resulting cubes
Min_CubeXorVar( pCube, Var0, v10 );
pCube->nLits -= (v00 != 3);
pCube->nLits += ((v00 ^ v10) != 3);
Min_CubeXorVar( pThis, Var1, v01 );
pThis->nLits -= (v11 != 3);
pThis->nLits += ((v01 ^ v11) != 3);
// add the cubes
nCubesOld = p->nCubes;
Min_EsopAddCube( p, pCube );
Min_EsopAddCube( p, pThis );
// check if the cubes were absorbed
if ( p->nCubes < nCubesOld + 2 )
continue;
// pull out both cubes
assert( pThis == p->ppStore[pThis->nLits] );
p->ppStore[pThis->nLits] = pThis->pNext;
assert( pCube == p->ppStore[pCube->nLits] );
p->ppStore[pCube->nLits] = pCube->pNext;
p->nCubes -= 2;
// derive the second pair of resulting cubes
Min_CubeXorVar( pCube, Var0, v10 );
pCube->nLits -= ((v00 ^ v10) != 3);
pCube->nLits += (v00 != 3);
Min_CubeXorVar( pCube, Var1, v11 );
pCube->nLits -= (v01 != 3);
pCube->nLits += ((v01 ^ v11) != 3);
Min_CubeXorVar( pThis, Var0, v00 );
pThis->nLits -= (v10 != 3);
pThis->nLits += ((v00 ^ v10) != 3);
Min_CubeXorVar( pThis, Var1, v01 );
pThis->nLits -= ((v01 ^ v11) != 3);
pThis->nLits += (v11 != 3);
// add them anyhow
Min_EsopAddCube( p, pCube );
Min_EsopAddCube( p, pThis );
}
// printf( "Pairs = %d ", nPairs );
}
/**Function*************************************************************
Synopsis [Adds the cube to storage.]
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.
Do not forget to clean the storage!]
SideEffects []
SeeAlso []
***********************************************************************/
int Min_EsopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
{
Min_Cube_t * pThis, ** ppPrev;
// try to find the identical cube
Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
{
if ( Min_CubesAreEqual( pCube, pThis ) )
{
*ppPrev = pThis->pNext;
Min_CubeRecycle( p, pCube );
Min_CubeRecycle( p, pThis );
p->nCubes--;
return 0;
}
}
// find a distance-1 cube if it exists
if ( pCube->nLits < pCube->nVars )
Min_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev )
{
if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
{
*ppPrev = pThis->pNext;
Min_CubesTransform( pCube, pThis, p->pTemp );
pCube->nLits++;
Min_CubeRecycle( p, pThis );
p->nCubes--;
return 1;
}
}
Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
{
if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
{
*ppPrev = pThis->pNext;
Min_CubesTransform( pCube, pThis, p->pTemp );
pCube->nLits--;
Min_CubeRecycle( p, pThis );
p->nCubes--;
return 1;
}
}
if ( pCube->nLits > 0 )
Min_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev )
{
if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
{
*ppPrev = pThis->pNext;
Min_CubesTransform( pCube, pThis, p->pTemp );
Min_CubeRecycle( p, pThis );
p->nCubes--;
return 1;
}
}
// 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_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
{
assert( pCube != p->pBubble );
assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
while ( Min_EsopAddCubeInt( p, pCube ) );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END