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

  FileName    [cnfCut.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [AIG-to-CNF conversion.]

  Synopsis    []

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - April 28, 2007.]

  Revision    [$Id: cnfCut.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]

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

#include "cnf.h"
#include "bool/kit/kit.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [Allocates cut of the given size.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Cnf_Cut_t * Cnf_CutAlloc( Cnf_Man_t * p, int nLeaves )
{
    Cnf_Cut_t * pCut;
    int nSize = sizeof(Cnf_Cut_t) + sizeof(int) * nLeaves + sizeof(unsigned) * Abc_TruthWordNum(nLeaves);
    pCut = (Cnf_Cut_t *)Aig_MmFlexEntryFetch( p->pMemCuts, nSize );
    pCut->nFanins = nLeaves;
    pCut->nWords = Abc_TruthWordNum(nLeaves);
    pCut->vIsop[0] = pCut->vIsop[1] = NULL;
    return pCut;
}

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

  Synopsis    [Deallocates cut.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cnf_CutFree( Cnf_Cut_t * pCut )
{
    if ( pCut->vIsop[0] )
        Vec_IntFree( pCut->vIsop[0] );
    if ( pCut->vIsop[1] )
        Vec_IntFree( pCut->vIsop[1] );
}

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

  Synopsis    [Creates cut for the given node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj )
{
    Dar_Cut_t * pCutBest;
    Cnf_Cut_t * pCut;
    unsigned * pTruth;
    assert( Aig_ObjIsNode(pObj) );
    pCutBest = Dar_ObjBestCut( pObj );
    assert( pCutBest != NULL );
    assert( pCutBest->nLeaves <= 4 );
    pCut = Cnf_CutAlloc( p, pCutBest->nLeaves );
    memcpy( pCut->pFanins, pCutBest->pLeaves, sizeof(int) * pCutBest->nLeaves );
    pTruth = Cnf_CutTruth(pCut);
    *pTruth = (pCutBest->uTruth << 16) | pCutBest->uTruth;
    pCut->Cost = Cnf_CutSopCost( p, pCutBest );
    return pCut;
}

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

  Synopsis    [Deallocates cut.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cnf_CutPrint( Cnf_Cut_t * pCut )
{
    int i;
    printf( "{" );
    for ( i = 0; i < pCut->nFanins; i++ )
        printf( "%d ", pCut->pFanins[i] );
    printf( " } " );
}

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

  Synopsis    [Allocates cut of the given size.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cnf_CutDeref( Cnf_Man_t * p, Cnf_Cut_t * pCut )
{
    Aig_Obj_t * pObj;
    int i;
    Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
    {
        assert( pObj->nRefs > 0 );
        pObj->nRefs--;
    }
}

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

  Synopsis    [Allocates cut of the given size.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cnf_CutRef( Cnf_Man_t * p, Cnf_Cut_t * pCut )
{
    Aig_Obj_t * pObj;
    int i;
    Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
    {
        pObj->nRefs++;
    }
}

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

  Synopsis    [Allocates cut of the given size.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cnf_CutUpdateRefs( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, Cnf_Cut_t * pCutRes )
{
    Cnf_CutDeref( p, pCut );
    Cnf_CutDeref( p, pCutFan );
    Cnf_CutRef( p, pCutRes );
}

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

  Synopsis    [Merges two arrays of integers.]

  Description [Returns the number of items.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Cnf_CutMergeLeaves( Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, int * pFanins )
{
    int i, k, nFanins = 0;
    for ( i = k = 0; i < pCut->nFanins && k < pCutFan->nFanins; )
    {
        if ( pCut->pFanins[i] == pCutFan->pFanins[k] )
            pFanins[nFanins++] = pCut->pFanins[i], i++, k++;
        else if ( pCut->pFanins[i] < pCutFan->pFanins[k] )
            pFanins[nFanins++] = pCut->pFanins[i], i++;
        else
            pFanins[nFanins++] = pCutFan->pFanins[k], k++;
    }
    for ( ; i < pCut->nFanins; i++ )
        pFanins[nFanins++] = pCut->pFanins[i];
    for ( ; k < pCutFan->nFanins; k++ )
        pFanins[nFanins++] = pCutFan->pFanins[k];
    return nFanins;
}

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

  Synopsis    [Computes the stretching phase of the cut w.r.t. the merged cut.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline unsigned Cnf_TruthPhase( Cnf_Cut_t * pCut, Cnf_Cut_t * pCut1 )
{
    unsigned uPhase = 0;
    int i, k;
    for ( i = k = 0; i < pCut->nFanins; i++ )
    {
        if ( k == pCut1->nFanins )
            break;
        if ( pCut->pFanins[i] < pCut1->pFanins[k] )
            continue;
        assert( pCut->pFanins[i] == pCut1->pFanins[k] );
        uPhase |= (1 << i);
        k++;
    }
    return uPhase;
}

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

  Synopsis    [Removes the fanin variable.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cnf_CutRemoveIthVar( Cnf_Cut_t * pCut, int iVar, int iFan )
{
    int i;
    assert( pCut->pFanins[iVar] == iFan );
    pCut->nFanins--;
    for ( i = iVar; i < pCut->nFanins; i++ )
        pCut->pFanins[i] = pCut->pFanins[i+1];
}

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

  Synopsis    [Inserts the fanin variable.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cnf_CutInsertIthVar( Cnf_Cut_t * pCut, int iVar, int iFan )
{
    int i;
    for ( i = pCut->nFanins; i > iVar; i-- )
        pCut->pFanins[i] = pCut->pFanins[i-1];
    pCut->pFanins[iVar] = iFan;
    pCut->nFanins++;
}

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

  Synopsis    [Merges two cuts.]

  Description [Returns NULL of the cuts cannot be merged.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Cnf_Cut_t * Cnf_CutCompose( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, int iFan )
{
    Cnf_Cut_t * pCutRes;
    static int pFanins[32];
    unsigned * pTruth, * pTruthFan, * pTruthRes;
    unsigned * pTop = p->pTruths[0], * pFan = p->pTruths[2], * pTemp = p->pTruths[3];
    unsigned uPhase, uPhaseFan;
    int i, iVar, nFanins, RetValue;

    // make sure the second cut is the fanin of the first
    for ( iVar = 0; iVar < pCut->nFanins; iVar++ )
        if ( pCut->pFanins[iVar] == iFan )
            break;
    assert( iVar < pCut->nFanins );
    // remove this variable
    Cnf_CutRemoveIthVar( pCut, iVar, iFan );
    // merge leaves of the cuts
    nFanins = Cnf_CutMergeLeaves( pCut, pCutFan, pFanins );
    if ( nFanins+1 > p->nMergeLimit )
    {
        Cnf_CutInsertIthVar( pCut, iVar, iFan );
        return NULL;
    }
    // create new cut
    pCutRes = Cnf_CutAlloc( p, nFanins );
    memcpy( pCutRes->pFanins, pFanins, sizeof(int) * nFanins );
    assert( pCutRes->nFanins <= pCut->nFanins + pCutFan->nFanins );

    // derive its truth table
    // get the truth tables in the composition space
    pTruth    = Cnf_CutTruth(pCut);
    pTruthFan = Cnf_CutTruth(pCutFan);
    pTruthRes = Cnf_CutTruth(pCutRes);
    for ( i = 0; i < 2*pCutRes->nWords; i++ )
        pTop[i] = pTruth[i % pCut->nWords];
    for ( i = 0; i < pCutRes->nWords; i++ )
        pFan[i] = pTruthFan[i % pCutFan->nWords];
    // move the variable to the end
    uPhase = Kit_BitMask( pCutRes->nFanins+1 ) & ~(1 << iVar);
    Kit_TruthShrink( pTemp, pTop, pCutRes->nFanins, pCutRes->nFanins+1, uPhase, 1 );
    // compute the phases
    uPhase    = Cnf_TruthPhase( pCutRes, pCut    ) | (1 << pCutRes->nFanins);
    uPhaseFan = Cnf_TruthPhase( pCutRes, pCutFan );
    // permute truth-tables to the common support
    Kit_TruthStretch( pTemp, pTop, pCut->nFanins+1,  pCutRes->nFanins+1, uPhase,    1 );
    Kit_TruthStretch( pTemp, pFan, pCutFan->nFanins, pCutRes->nFanins,   uPhaseFan, 1 );
    // perform Boolean operation
    Kit_TruthMux( pTruthRes, pTop, pTop+pCutRes->nWords, pFan, pCutRes->nFanins );
    // return the cut to its original condition
    Cnf_CutInsertIthVar( pCut, iVar, iFan );
    // consider the simple case
    if ( pCutRes->nFanins < 5 )
    {
        pCutRes->Cost = p->pSopSizes[0xFFFF & *pTruthRes] + p->pSopSizes[0xFFFF & ~*pTruthRes];
        return pCutRes;
    }

    // derive ISOP for positive phase
    RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
    pCutRes->vIsop[1] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
    // derive ISOP for negative phase
    Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
    RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
    pCutRes->vIsop[0] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
    Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );

    // compute the cut cost
    if ( pCutRes->vIsop[0] == NULL || pCutRes->vIsop[1] == NULL )
        pCutRes->Cost = 127;
    else if ( Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]) > 127 )
        pCutRes->Cost = 127;
    else
        pCutRes->Cost = Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]);
    return pCutRes;
}

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


ABC_NAMESPACE_IMPL_END