/**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