/**CFile****************************************************************

  FileName    [covBuild.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Mapping into network of SOPs/ESOPs.]

  Synopsis    [Network construction procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: covBuild.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "cov.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Derives the decomposed network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Obj_t * Abc_NtkCovDeriveCube( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp, int fCompl )
{
    Vec_Int_t * vLits;
    Abc_Obj_t * pNodeNew, * pFanin;
    int i, iFanin, Lit;
    // create empty cube
    if ( pCube->nLits == 0 )
    {
        if ( fCompl )
            return Abc_NtkCreateNodeConst0(pNtkNew);
        return Abc_NtkCreateNodeConst1(pNtkNew);
    }
    // get the literals of this cube
    vLits = Vec_IntAlloc( 10 );
    Min_CubeGetLits( pCube, vLits );
    assert( pCube->nLits == (unsigned)vLits->nSize );
    // create special case when there is only one literal
    if ( pCube->nLits == 1 )
    {
        iFanin = Vec_IntEntry(vLits,0);
        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
        Lit = Min_CubeGetVar(pCube, iFanin);
        assert( Lit == 1 || Lit == 2 );
        Vec_IntFree( vLits );
        if ( (Lit == 1) ^ fCompl )// negative
            return Abc_NtkCreateNodeInv( pNtkNew, pFanin->pCopy );
        return pFanin->pCopy;
    }
    assert( pCube->nLits > 1 );
    // create the AND cube
    pNodeNew = Abc_NtkCreateNode( pNtkNew );
    for ( i = 0; i < vLits->nSize; i++ )
    {
        iFanin = Vec_IntEntry(vLits,i);
        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
        Lit = Min_CubeGetVar(pCube, iFanin);
        assert( Lit == 1 || Lit == 2 );
        Vec_IntWriteEntry( vLits, i, Lit==1 );
        Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
    }
    pNodeNew->pData = Abc_SopCreateAnd( (Mem_Flex_t *)pNtkNew->pManFunc, vLits->nSize, vLits->pArray );
    if ( fCompl )
        Abc_SopComplement( (char *)pNodeNew->pData );
    Vec_IntFree( vLits );
    return pNodeNew;
}

/**Function*************************************************************

  Synopsis    [Derives the decomposed network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Obj_t * Abc_NtkCovDeriveNode_rec( Cov_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int Level )
{
    Min_Cube_t * pCover, * pCube;
    Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin;
    Vec_Int_t * vSupp;
    int Entry, nCubes, i;

    if ( Abc_ObjIsCi(pObj) )
        return pObj->pCopy;
    assert( Abc_ObjIsNode(pObj) );
    // skip if already computed
    if ( pObj->pCopy )
        return pObj->pCopy;

    // get the support and the cover
    vSupp  = Abc_ObjGetSupp( pObj ); 
    pCover = Abc_ObjGetCover2( pObj );
    assert( vSupp );
/*
    if ( pCover &&  pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) > 0 )
    {
        printf( "%d\n ", pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) );
        Min_CoverWrite( stdout, pCover );
    }
*/
/*
    // print the support of this node
    printf( "{ " );
    Vec_IntForEachEntry( vSupp, Entry, i )
        printf( "%d ", Entry );
    printf( "}  cubes = %d\n", Min_CoverCountCubes( pCover ) );
*/
    // process the fanins
    Vec_IntForEachEntry( vSupp, Entry, i )
    {
        pFanin = Abc_NtkObj(pObj->pNtk, Entry);
        Abc_NtkCovDeriveNode_rec( p, pNtkNew, pFanin, Level+1 );
    }

    // for each cube, construct the node
    nCubes = Min_CoverCountCubes( pCover );
    if ( nCubes == 0 )
        pNodeNew = Abc_NtkCreateNodeConst0(pNtkNew);
    else if ( nCubes == 1 )
        pNodeNew = Abc_NtkCovDeriveCube( pNtkNew, pObj, pCover, vSupp, 0 );
    else
    {
        pNodeNew = Abc_NtkCreateNode( pNtkNew );
        Min_CoverForEachCube( pCover, pCube )
        {
            pFaninNew = Abc_NtkCovDeriveCube( pNtkNew, pObj, pCube, vSupp, 0 );
            Abc_ObjAddFanin( pNodeNew, pFaninNew );
        }
        pNodeNew->pData = Abc_SopCreateXorSpecial( (Mem_Flex_t *)pNtkNew->pManFunc, nCubes );
    }
/*
    printf( "Created node %d(%d) at level %d: ", pNodeNew->Id, pObj->Id, Level );
    Vec_IntForEachEntry( vSupp, Entry, i )
    {
        pFanin = Abc_NtkObj(pObj->pNtk, Entry);
        printf( "%d(%d) ", pFanin->pCopy->Id, pFanin->Id );
    }
    printf( "\n" );
    Min_CoverWrite( stdout, pCover );
*/
    pObj->pCopy = pNodeNew;
    return pNodeNew;
}

/**Function*************************************************************

  Synopsis    [Derives the decomposed network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkCovDerive( Cov_Man_t * p, Abc_Ntk_t * pNtk )
{
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pObj;
    int i;
    assert( Abc_NtkIsStrash(pNtk) );
    // perform strashing
    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
    // reconstruct the network
    Abc_NtkForEachCo( pNtk, pObj, i )
    {
        Abc_NtkCovDeriveNode_rec( p, pNtkNew, Abc_ObjFanin0(pObj), 0 );
//        printf( "*** CO %s : %d -> %d \n", Abc_ObjName(pObj), pObj->pCopy->Id, Abc_ObjFanin0(pObj)->pCopy->Id );
    }
    // add the COs
    Abc_NtkFinalize( pNtk, pNtkNew );
    Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
    // make sure everything is okay
    if ( !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkCovDerive: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
        return NULL;
    }
    return pNtkNew;
}




/**Function*************************************************************

  Synopsis    [Derives the decomposed network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Obj_t * Abc_NtkCovDeriveInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl )
{
    assert( pObj->pCopy );
    if ( !fCompl )
        return pObj->pCopy;
    if ( pObj->pCopy->pCopy == NULL )
        pObj->pCopy->pCopy = Abc_NtkCreateNodeInv( pNtkNew, pObj->pCopy );
    return pObj->pCopy->pCopy;
 }

/**Function*************************************************************

  Synopsis    [Derives the decomposed network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Obj_t * Abc_NtkCovDeriveCubeInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp )
{
    Vec_Int_t * vLits;
    Abc_Obj_t * pNodeNew, * pFanin;
    int i, iFanin, Lit;
    // create empty cube
    if ( pCube->nLits == 0 )
        return Abc_NtkCreateNodeConst1(pNtkNew);
    // get the literals of this cube
    vLits = Vec_IntAlloc( 10 );
    Min_CubeGetLits( pCube, vLits );
    assert( pCube->nLits == (unsigned)vLits->nSize );
    // create special case when there is only one literal
    if ( pCube->nLits == 1 )
    {
        iFanin = Vec_IntEntry(vLits,0);
        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
        Lit = Min_CubeGetVar(pCube, iFanin);
        assert( Lit == 1 || Lit == 2 );
        Vec_IntFree( vLits );
//        if ( Lit == 1 )// negative
//            return Abc_NtkCreateNodeInv( pNtkNew, pFanin->pCopy );
//        return pFanin->pCopy;
        return Abc_NtkCovDeriveInv( pNtkNew, pFanin, Lit==1 );
    }
    assert( pCube->nLits > 1 );
    // create the AND cube
    pNodeNew = Abc_NtkCreateNode( pNtkNew );
    for ( i = 0; i < vLits->nSize; i++ )
    {
        iFanin = Vec_IntEntry(vLits,i);
        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
        Lit = Min_CubeGetVar(pCube, iFanin);
        assert( Lit == 1 || Lit == 2 );
        Vec_IntWriteEntry( vLits, i, Lit==1 );
//        Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
        Abc_ObjAddFanin( pNodeNew, Abc_NtkCovDeriveInv( pNtkNew, pFanin, Lit==1 ) );
    }
//    pNodeNew->pData = Abc_SopCreateAnd( (Mem_Flex_t *)pNtkNew->pManFunc, vLits->nSize, vLits->pArray );
    pNodeNew->pData = Abc_SopCreateAnd( (Mem_Flex_t *)pNtkNew->pManFunc, vLits->nSize, NULL );
    Vec_IntFree( vLits );
    return pNodeNew;
}

/**Function*************************************************************

  Synopsis    [Derives the decomposed network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Obj_t * Abc_NtkCovDeriveNodeInv_rec( Cov_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl )
{
    Min_Cube_t * pCover, * pCube;
    Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin;
    Vec_Int_t * vSupp;
    int Entry, nCubes, i;

    // skip if already computed
    if ( pObj->pCopy )
        return Abc_NtkCovDeriveInv( pNtkNew, pObj, fCompl );
    assert( Abc_ObjIsNode(pObj) );

    // get the support and the cover
    vSupp  = Abc_ObjGetSupp( pObj ); 
    pCover = Abc_ObjGetCover2( pObj );
    assert( vSupp );

    // process the fanins
    Vec_IntForEachEntry( vSupp, Entry, i )
    {
        pFanin = Abc_NtkObj(pObj->pNtk, Entry);
        Abc_NtkCovDeriveNodeInv_rec( p, pNtkNew, pFanin, 0 );
    }

    // for each cube, construct the node
    nCubes = Min_CoverCountCubes( pCover );
    if ( nCubes == 0 )
        pNodeNew = Abc_NtkCreateNodeConst0(pNtkNew);
    else if ( nCubes == 1 )
        pNodeNew = Abc_NtkCovDeriveCubeInv( pNtkNew, pObj, pCover, vSupp );
    else
    {
        pNodeNew = Abc_NtkCreateNode( pNtkNew );
        Min_CoverForEachCube( pCover, pCube )
        {
            pFaninNew = Abc_NtkCovDeriveCubeInv( pNtkNew, pObj, pCube, vSupp );
            Abc_ObjAddFanin( pNodeNew, pFaninNew );
        }
        pNodeNew->pData = Abc_SopCreateXorSpecial( (Mem_Flex_t *)pNtkNew->pManFunc, nCubes );
    }

    pObj->pCopy = pNodeNew;
    return Abc_NtkCovDeriveInv( pNtkNew, pObj, fCompl );
}

/**Function*************************************************************

  Synopsis    [Derives the decomposed network.]

  Description [The resulting network contains only pure AND/OR/EXOR gates
  and inverters. This procedure is usedful to generate Verilog.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkCovDeriveClean( Cov_Man_t * p, Abc_Ntk_t * pNtk )
{
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pObj, * pNodeNew;
    int i;
    assert( Abc_NtkIsStrash(pNtk) );
    // perform strashing
    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
    // reconstruct the network
    Abc_NtkForEachCo( pNtk, pObj, i )
    {
        pNodeNew = Abc_NtkCovDeriveNodeInv_rec( p, pNtkNew, Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );
        Abc_ObjAddFanin( pObj->pCopy, pNodeNew );
    }
    // add the COs
    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
    // make sure everything is okay
    if ( !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkCovDeriveInv: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
        return NULL;
    }
    return pNtkNew;
}



/**Function*************************************************************

  Synopsis    [Derives the decomposed network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Obj_t * Abc_NtkCovDerive_rec( Cov_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
{
    int fVerbose = 0;
    Min_Cube_t * pCover, * pCovers[3];
    Abc_Obj_t * pNodeNew, * pFanin;
    Vec_Int_t * vSupp;
    Vec_Str_t * vCover;
    int i, Entry, nCubes, Type;
    // skip if already computed
    if ( pObj->pCopy )
        return pObj->pCopy;
    assert( Abc_ObjIsNode(pObj) );
    // get the support and the cover
    vSupp  = Abc_ObjGetSupp( pObj ); 
    assert( vSupp );
    // choose the cover to implement
    pCovers[0] = Abc_ObjGetCover( pObj, 0 );
    pCovers[1] = Abc_ObjGetCover( pObj, 1 );
    pCovers[2] = Abc_ObjGetCover2( pObj );
    // use positive polarity
    if ( pCovers[0] 
        && (!pCovers[1] || Min_CoverCountCubes(pCovers[0]) <= Min_CoverCountCubes(pCovers[1]))
        && (!pCovers[2] || Min_CoverCountCubes(pCovers[0]) <= Min_CoverCountCubes(pCovers[2]))   )
    {
        pCover = pCovers[0];
        Type = '1';
    }
    else 
    // use negative polarity
    if ( pCovers[1] 
        && (!pCovers[0] || Min_CoverCountCubes(pCovers[1]) <= Min_CoverCountCubes(pCovers[0]))
        && (!pCovers[2] || Min_CoverCountCubes(pCovers[1]) <= Min_CoverCountCubes(pCovers[2]))   )
    {
        pCover = pCovers[1];
        Type = '0';
    }
    else 
    // use XOR polarity
    if ( pCovers[2] 
        && (!pCovers[0] || Min_CoverCountCubes(pCovers[2]) < Min_CoverCountCubes(pCovers[0]))
        && (!pCovers[1] || Min_CoverCountCubes(pCovers[2]) < Min_CoverCountCubes(pCovers[1]))   )
    {
        pCover = pCovers[2];
        Type = 'x';
    }
    else
        assert( 0 );
    // print the support of this node
    if ( fVerbose )
    {
        printf( "{ " );
        Vec_IntForEachEntry( vSupp, Entry, i )
            printf( "%d ", Entry );
        printf( "}  cubes = %d\n", Min_CoverCountCubes( pCover ) );
    }
    // process the fanins
    Vec_IntForEachEntry( vSupp, Entry, i )
    {
        pFanin = Abc_NtkObj(pObj->pNtk, Entry);
        Abc_NtkCovDerive_rec( p, pNtkNew, pFanin );
    }
    // for each cube, construct the node
    nCubes = Min_CoverCountCubes( pCover );
    if ( nCubes == 0 )
        pNodeNew = Abc_NtkCreateNodeConst0(pNtkNew);
    else if ( nCubes == 1 )
        pNodeNew = Abc_NtkCovDeriveCube( pNtkNew, pObj, pCover, vSupp, Type == '0' );
    else
    {
        // create the node
        pNodeNew = Abc_NtkCreateNode( pNtkNew );
        Vec_IntForEachEntry( vSupp, Entry, i )
        {
            pFanin = Abc_NtkObj(pObj->pNtk, Entry);
            Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
        }
        // derive the function
        vCover = Vec_StrAlloc( 100 );
        Min_CoverCreate( vCover, pCover, (char)Type );
        pNodeNew->pData = Abc_SopRegister((Mem_Flex_t *)pNtkNew->pManFunc, Vec_StrArray(vCover) );
        Vec_StrFree( vCover );
    }

/*
    printf( "Created node %d(%d) at level %d: ", pNodeNew->Id, pObj->Id, Level );
    Vec_IntForEachEntry( vSupp, Entry, i )
    {
        pFanin = Abc_NtkObj(pObj->pNtk, Entry);
        printf( "%d(%d) ", pFanin->pCopy->Id, pFanin->Id );
    }
    printf( "\n" );
    Min_CoverWrite( stdout, pCover );
*/
    return pObj->pCopy = pNodeNew;
}

/**Function*************************************************************

  Synopsis    [Derives the decomposed network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Abc_NtkCovDeriveRegular( Cov_Man_t * p, Abc_Ntk_t * pNtk )
{
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pObj, * pNodeNew;
    int i;
    assert( Abc_NtkIsStrash(pNtk) );
    // perform strashing
    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
    // reconstruct the network
    if ( Abc_ObjFanoutNum(Abc_AigConst1(pNtk)) > 0 )
        Abc_AigConst1(pNtk)->pCopy = Abc_NtkCreateNodeConst1(pNtkNew);
    Abc_NtkForEachCo( pNtk, pObj, i )
    {
        pNodeNew = Abc_NtkCovDerive_rec( p, pNtkNew, Abc_ObjFanin0(pObj) );
        if ( Abc_ObjFaninC0(pObj) )
        {
            if ( pNodeNew->pData && Abc_ObjFanoutNum(Abc_ObjFanin0(pObj)) == 1 )
                Abc_SopComplement( (char *)pNodeNew->pData );
            else
                pNodeNew = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew );
        }
        Abc_ObjAddFanin( pObj->pCopy, pNodeNew );
    }
    // add the COs
    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
    // make sure everything is okay
    if ( !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkCovDerive: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
        return NULL;
    }
    return pNtkNew;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END