/**CFile****************************************************************
Copyright (c) The Regents of the University of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or
royalty fees, to use, copy, modify, and distribute this software and its
documentation for any purpose, provided that the above copyright notice and
the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF
THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING,
BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS,
AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE,
SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.


  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 "kit.h"

////////////////////////////////////////////////////////////////////////
///                        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) * Aig_TruthWordNum(nLeaves);
    pCut = (Cnf_Cut_t *)Aig_MmFlexEntryFetch( p->pMemCuts, nSize );
    pCut->nFanins = nLeaves;
    pCut->nWords = Aig_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 THREAD_LOCAL 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                                ///
////////////////////////////////////////////////////////////////////////