text: /**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 "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 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                                ///
  ////////////////////////////////////////////////////////////////////////
  
  
  