text: /**CFile****************************************************************
  
    FileName    [giaEsop.c]
  
    SystemName  [ABC: Logic synthesis and verification system.]
  
    PackageName [Scalable AIG package.]
  
    Synopsis    [ESOP computation.]
  
    Author      [Alan Mishchenko]
    
    Affiliation [UC Berkeley]
  
    Date        [Ver. 1.0. Started - June 20, 2005.]
  
    Revision    [$Id: giaEsop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
  
  ***********************************************************************/
  
  #include "gia.h"
  #include "misc/extra/extra.h"
  #include "misc/vec/vecHsh.h"
  #include "misc/vec/vecWec.h"
  
  ABC_NAMESPACE_IMPL_START
  
  
  ////////////////////////////////////////////////////////////////////////
  ///                        DECLARATIONS                              ///
  ////////////////////////////////////////////////////////////////////////
  
  typedef struct Eso_Man_t_ Eso_Man_t;
  struct Eso_Man_t_
  {
      Gia_Man_t *     pGia;     // user's AIG
      int             nVars;    // number of variables
      int             Cube1;    // ID of const1 cube
      Vec_Wec_t *     vEsops;   // ESOP for each node
      Hsh_VecMan_t *  pHash;    // hash table for cubes
      Vec_Wec_t *     vCubes;   // cover during minimization
      // internal
      Vec_Int_t *     vCube1;   // first cube
      Vec_Int_t *     vCube2;   // second cube
      Vec_Int_t *     vCube;    // resulting cube
  };
  
  static inline Vec_Int_t * Eso_ManCube( Eso_Man_t * p, int iCube ) { assert( iCube >= 0 ); return Hsh_VecReadEntry(p->pHash, iCube); }
  
  ////////////////////////////////////////////////////////////////////////
  ///                     FUNCTION DEFINITIONS                         ///
  ////////////////////////////////////////////////////////////////////////
      
  /**Function*************************************************************
  
    Synopsis    [Computation manager.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  Eso_Man_t * Eso_ManAlloc( Gia_Man_t * pGia )
  {
      int i, n, Id;
      Eso_Man_t * p = ABC_CALLOC( Eso_Man_t, 1 );
      p->pGia   = pGia;
      p->nVars  = Gia_ManCiNum(pGia);
      p->Cube1  = ABC_INFINITY;
      p->vEsops = Vec_WecStart( Gia_ManObjNum(pGia) );
      p->pHash  = Hsh_VecManStart( 1000 );
      p->vCubes = Vec_WecStart(Gia_ManCiNum(pGia)+1);
      p->vCube1 = Vec_IntAlloc(Gia_ManCiNum(pGia));
      p->vCube2 = Vec_IntAlloc(Gia_ManCiNum(pGia));
      p->vCube  = Vec_IntAlloc(Gia_ManCiNum(pGia));
      Gia_ManForEachCiId( pGia, Id, i )
      {
          for ( n = 0; n < 2; n++ )
          {
              Vec_IntFill( p->vCube, 1, Abc_Var2Lit(i, n) );
              Hsh_VecManAdd( p->pHash, p->vCube );
          }
          Vec_IntPush( Vec_WecEntry(p->vEsops, Id), Abc_Var2Lit(i, 0) );
      }
      return p;
  }
  void Eso_ManStop( Eso_Man_t * p )
  {
      Vec_WecFree( p->vEsops );
      Hsh_VecManStop( p->pHash );
      Vec_WecFree( p->vCubes );
      Vec_IntFree( p->vCube1 );
      Vec_IntFree( p->vCube2 );
      Vec_IntFree( p->vCube );
      ABC_FREE( p );
  }
      
  
  /**Function*************************************************************
  
    Synopsis    [Printing/transforming the cover.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Eso_ManCoverPrint( Eso_Man_t * p, Vec_Int_t * vEsop )
  {
      Vec_Str_t * vStr;
      Vec_Int_t * vCube;
      int i, k, Lit, Cube;
      if ( Vec_IntSize(vEsop) == 0 )
      {
          printf( "Const 0\n" );
          return;
      }
      vStr = Vec_StrAlloc( p->nVars + 4 );
      Vec_StrFill( vStr, p->nVars, '-' );
      Vec_StrPush( vStr, ' ' );
      Vec_StrPush( vStr, '1' );
      Vec_StrPush( vStr, '\n' );
      Vec_StrPush( vStr, '\0' );
      assert( Vec_IntSize(vEsop) > 0 );
      Vec_IntForEachEntry( vEsop, Cube, i )
      {
          if ( Cube == p->Cube1 )
              printf( "%s", Vec_StrArray(vStr) );
          else 
          {
              vCube = Eso_ManCube( p, Cube );
              Vec_IntForEachEntry( vCube, Lit, k )
                  Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit)?'0':'1') );
              printf( "%s", Vec_StrArray(vStr) );
              Vec_IntForEachEntry( vCube, Lit, k )
                  Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), '-' );
          }
      }
      printf( "\n" );
      Vec_StrFree( vStr );
  }
  Vec_Wec_t * Eso_ManCoverDerive( Eso_Man_t * p, Vec_Ptr_t * vCover )
  {
      Vec_Wec_t * vRes;
      Vec_Int_t * vEsop, * vLevel;  int i;
      vRes = Vec_WecAlloc( Vec_VecSizeSize((Vec_Vec_t *)vCover) );
      Vec_PtrForEachEntry( Vec_Int_t *, vCover, vEsop, i )
      {
          if ( Vec_IntSize(vEsop) > 0 )
          {
              int c, Cube;
              Vec_IntForEachEntry( vEsop, Cube, c )
              {
                  vLevel = Vec_WecPushLevel( vRes );
                  if ( Cube != p->Cube1 )
                  {
                      int k, Lit;
                      Vec_Int_t * vCube = Eso_ManCube( p, Cube );
                      Vec_IntForEachEntry( vCube, Lit, k )
                          Vec_IntPush( vLevel, Lit );
                  }
                  Vec_IntPush( vLevel, -i-1 );
              }
          }
      }
      //assert( Abc_MaxInt(Vec_WecSize(vRes), 8) == Vec_WecCap(vRes) );
      return vRes;
  }
  Gia_Man_t * Eso_ManCoverConvert( Eso_Man_t * p, Vec_Ptr_t * vCover )
  {
      Vec_Int_t * vEsop;
      Gia_Man_t * pNew, * pTemp;
      Gia_Obj_t * pObj;  int i;
      pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) );
      pNew->pName = Abc_UtilStrsav( p->pGia->pName );
      pNew->pSpec = Abc_UtilStrsav( p->pGia->pSpec );
      Gia_ManHashAlloc( pNew );
      Gia_ManConst0(p->pGia)->Value = 0;
      Gia_ManForEachCi( p->pGia, pObj, i )
          pObj->Value = Gia_ManAppendCi(pNew);
      Vec_PtrForEachEntry( Vec_Int_t *, vCover, vEsop, i )
      {
          if ( Vec_IntSize(vEsop) > 0 )
          {
              int c, Cube, iRoot = 0;
              Vec_IntForEachEntry( vEsop, Cube, c )
              {
                  int k, Lit, iAnd = 1;
                  if ( Cube != p->Cube1 )
                  {
                      Vec_Int_t * vCube = Eso_ManCube( p, Cube );
                      Vec_IntForEachEntry( vCube, Lit, k )
                          iAnd = Gia_ManHashAnd( pNew, iAnd, Lit + 2 );
                  }
                  iRoot = Gia_ManHashXor( pNew, iRoot, iAnd );
              }
              Gia_ManAppendCo( pNew, iRoot );
          }
          else
              Gia_ManAppendCo( pNew, 0 );
      }
      // cleanup
      pNew = Gia_ManCleanup( pTemp = pNew );
      Gia_ManStop( pTemp );
      return pNew;
  }
  
  /**Function*************************************************************
  
    Synopsis    [Minimization.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  int Eso_ManFindDistOneLitEqual( int * pCube1, int * pCube2, int nLits ) // pCube1 and pCube2 both have nLits
  {
      int i, iDiff = -1;
      for ( i = 0; i < nLits; i++ )
          if ( pCube1[i] != pCube2[i] )
          {
              if ( iDiff != -1 )
                  return -1;
              if ( Abc_Lit2Var(pCube1[i]) != Abc_Lit2Var(pCube2[i]) )
                  return -1;
              iDiff = i;
          }
      return iDiff;
  }
  int Eso_ManFindDistOneLitNotEqual( int * pCube1, int * pCube2, int nLits ) // pCube1 has nLits; pCube2 has nLits + 1
  {
      int i, k, iDiff = -1;
      for ( i = k = 0; i < nLits; i++, k++ )
          if ( pCube1[i] != pCube2[k] )
          {
              if ( iDiff != -1 )
                  return -1;
              iDiff = i;
              i--;
          }
      if ( iDiff == -1 )
          iDiff = nLits;
      return iDiff;
  }
  void Eso_ManMinimizeAdd( Eso_Man_t * p, int Cube )
  {
      int fMimimize = 1;
      Vec_Int_t * vCube      = (Cube == p->Cube1) ? NULL : Eso_ManCube(p, Cube); 
      int * pCube2, * pCube  = (Cube == p->Cube1) ? NULL : Vec_IntArray(vCube); 
      int Cube2, nLits       = (Cube == p->Cube1) ? 0 : Vec_IntSize(vCube);
      Vec_Int_t * vLevel     = Vec_WecEntry( p->vCubes, nLits );
      int c, k, iLit, iPlace = Vec_IntFind( vLevel, Cube );
      if ( iPlace >= 0 ) // identical found
      {
          Vec_IntDrop( vLevel, iPlace );
          return;
      }
      if ( Cube == p->Cube1 ) // simple case
      {
          assert( Vec_IntSize(vLevel) == 0 );
          Vec_IntPush( vLevel, Cube );
          return;
      }
      // look for distance-1 in next bin
      if ( fMimimize && nLits < p->nVars - 1 )
      {
          Vec_Int_t * vLevel = Vec_WecEntry( p->vCubes, nLits+1 );
          Vec_IntForEachEntry( vLevel, Cube2, c )
          {
              pCube2 = Hsh_VecReadArray( p->pHash, Cube2 ); 
              iLit = Eso_ManFindDistOneLitNotEqual( pCube, pCube2, nLits );
              if ( iLit == -1 )
                  continue;
              // remove this cube
              Vec_IntDrop( vLevel, c );
              // create new cube
              Vec_IntClear( p->vCube );
              for ( k = 0; k <= nLits; k++ )
                  Vec_IntPush( p->vCube, Abc_LitNotCond(pCube2[k], k == iLit) );
              Cube = Hsh_VecManAdd( p->pHash, p->vCube );
              // try to add new cube
              Eso_ManMinimizeAdd( p, Cube );
              return;
          }
      }
      // look for distance-1 in the same bin
      if ( fMimimize )
      {
          Vec_IntForEachEntry( vLevel, Cube2, c )
          {
              pCube2 = Hsh_VecReadArray( p->pHash, Cube2 ); 
              iLit = Eso_ManFindDistOneLitEqual( pCube2, pCube, nLits );
              if ( iLit == -1 )
                  continue;
              // remove this cube
              Vec_IntDrop( vLevel, c );
              // create new cube
              Vec_IntClear( p->vCube );
              for ( k = 0; k < nLits; k++ )
                  if ( k != iLit )
                      Vec_IntPush( p->vCube, pCube[k] );
              if ( Vec_IntSize(p->vCube) == 0 )
                  Cube = p->Cube1;
              else
                  Cube = Hsh_VecManAdd( p->pHash, p->vCube );
              // try to add new cube
              Eso_ManMinimizeAdd( p, Cube );
              return;
          }
      }
      assert( nLits > 0 );
      if ( fMimimize && nLits > 0 )
      {
          // look for distance-1 in the previous bin
          Vec_Int_t * vLevel = Vec_WecEntry( p->vCubes, nLits-1 );
          // check for the case of one-literal cube
          if ( nLits == 1 && Vec_IntSize(vLevel) == 1 )
          {
              Vec_IntDrop( vLevel, 0 );
              Cube = Abc_LitNot( Cube );
          }
          else
          Vec_IntForEachEntry( vLevel, Cube2, c )
          {
              pCube2 = Hsh_VecReadArray( p->pHash, Cube2 ); 
              iLit = Eso_ManFindDistOneLitNotEqual( pCube2, pCube, nLits-1 );
              if ( iLit == -1 )
                  continue;
              // remove this cube
              Vec_IntDrop( vLevel, c );
              // create new cube
              Vec_IntClear( p->vCube );
              for ( k = 0; k < nLits; k++ )
                  Vec_IntPush( p->vCube, Abc_LitNotCond(pCube[k], k == iLit) );
              Cube = Hsh_VecManAdd( p->pHash, p->vCube );
              // try to add new cube
              Eso_ManMinimizeAdd( p, Cube );
              return;
          }
      }
      // could not find - simply add this cube
      Vec_IntPush( vLevel, Cube );
  }
  
  void Eso_ManMinimizeCopy( Eso_Man_t * p, Vec_Int_t * vEsop )
  {
      Vec_Int_t * vLevel;
      int i;
      Vec_IntClear( vEsop );
      Vec_WecForEachLevel( p->vCubes, vLevel, i )
      {
          Vec_IntAppend( vEsop, vLevel );
          if ( i > 0 )
          {
              int k, Cube;
              Vec_IntForEachEntry( vLevel, Cube, k )
                  assert( Vec_IntSize(Eso_ManCube(p, Cube)) == i );
          }
          Vec_IntClear( vLevel );
      }
  }
  
  /**Function*************************************************************
  
    Synopsis    [Compute the produce of two covers.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  int Eso_ManComputeAnd( Eso_Man_t * p, Vec_Int_t * vCube1, Vec_Int_t * vCube2, Vec_Int_t * vCube )
  {
      int * pBeg  = vCube->pArray;
      int * pBeg1 = vCube1->pArray;
      int * pBeg2 = vCube2->pArray;
      int * pEnd1 = vCube1->pArray + vCube1->nSize;
      int * pEnd2 = vCube2->pArray + vCube2->nSize;
      while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
      {
          if ( *pBeg1 == *pBeg2 )
              *pBeg++ = *pBeg1++, pBeg2++;
          else if ( Abc_Lit2Var(*pBeg1) == Abc_Lit2Var(*pBeg2) )
              return -1;
          else if ( *pBeg1 < *pBeg2 )
              *pBeg++ = *pBeg1++;
          else 
              *pBeg++ = *pBeg2++;
      }
      while ( pBeg1 < pEnd1 )
          *pBeg++ = *pBeg1++;
      while ( pBeg2 < pEnd2 )
          *pBeg++ = *pBeg2++;
      vCube->nSize = pBeg - vCube->pArray;
      assert( vCube->nSize <= vCube->nCap );
      assert( vCube->nSize >= vCube1->nSize );
      assert( vCube->nSize >= vCube2->nSize );
      return Hsh_VecManAdd( p->pHash, vCube );
  }
  void Eso_ManComputeOne( Eso_Man_t * p, Vec_Int_t * vEsop1, Vec_Int_t * vEsop2, Vec_Int_t * vEsop )
  {
      Vec_Int_t vCube1, vCube2;
      int i, k, Cube1, Cube2, Cube;
      Vec_IntClear( vEsop );
      if ( Vec_IntSize(vEsop1) == 0 || Vec_IntSize(vEsop2) == 0 )
          return;
      Cube1 = Vec_IntEntry(vEsop1, 0);
      Cube2 = Vec_IntEntry(vEsop2, 0);
      Vec_IntForEachEntry( vEsop1, Cube1, i )
      {
          if ( Cube1 == p->Cube1 )
          {
              Vec_IntForEachEntry( vEsop2, Cube2, k )
                  Eso_ManMinimizeAdd( p, Cube2 );
              continue;
          }
          Vec_IntForEachEntry( vEsop2, Cube2, k )
          {
              if ( Cube2 == p->Cube1 )
              {
                  Eso_ManMinimizeAdd( p, Cube1 );
                  continue;
              }
              vCube1 = *Hsh_VecReadEntry( p->pHash, Cube1 );
              vCube2 = *Hsh_VecReadEntry( p->pHash, Cube2 );
              Cube = Eso_ManComputeAnd( p, &vCube1, &vCube2, p->vCube );
              if ( Cube >= 0 )
                  Eso_ManMinimizeAdd( p, Cube );
          }
      }
      Eso_ManMinimizeCopy( p, vEsop );
  }
  
  /**Function*************************************************************
  
    Synopsis    [Complements the cover if needed, or just copy it.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  Vec_Int_t * Eso_ManTransformOne( Eso_Man_t * p, Vec_Int_t * vEsop, int fCompl, Vec_Int_t * vRes )
  {
      int i, Cube, Start = 0;
      Vec_IntClear( vRes );
      if ( fCompl )
      {
          if ( Vec_IntSize(vEsop) == 0 )
              Vec_IntPush( vRes, p->Cube1 );
          else
          {
              Cube = Vec_IntEntry(vEsop, 0);
              if ( Cube == p->Cube1 )
                  Start = 1;
              else if ( Cube < 2 * p->nVars )
                  Vec_IntPush( vRes, Abc_LitNot(Cube) ), Start = 1;
              else
                  Vec_IntPush( vRes, p->Cube1 );
          }
      }
      Vec_IntForEachEntryStart( vEsop, Cube, i, Start )
          Vec_IntPush( vRes, Cube );
      return vRes;
  }
  
  /**Function*************************************************************
  
    Synopsis    [Computes ESOP from AIG.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose, Vec_Wec_t ** pvRes )
  {
      abctime clk = Abc_Clock();
      Vec_Ptr_t * vCover;
      Gia_Man_t * pNew = NULL;
      Gia_Obj_t * pObj; 
      int i, nCubes = 0, nCubesUsed = 0;
      Vec_Int_t * vEsop1, * vEsop2, * vEsop;
      Eso_Man_t * p = Eso_ManAlloc( pGia ); 
      Gia_ManForEachAnd( pGia, pObj, i )
      {
          vEsop1 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId0(pObj, i) );
          vEsop2 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId1(pObj, i) );
          vEsop1 = Eso_ManTransformOne( p, vEsop1, Gia_ObjFaninC0(pObj), p->vCube1 );
          vEsop2 = Eso_ManTransformOne( p, vEsop2, Gia_ObjFaninC1(pObj), p->vCube2 );
          vEsop  = Vec_WecEntry( p->vEsops, i );
          Eso_ManComputeOne( p, vEsop1, vEsop2, vEsop );
          nCubes += Vec_IntSize(vEsop);
      }
      vCover = Vec_PtrAlloc( Gia_ManCoNum(pGia) );
      Gia_ManForEachCo( pGia, pObj, i )
      {
          vEsop1 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId0p(pGia, pObj) );
          vEsop1 = Eso_ManTransformOne( p, vEsop1, Gia_ObjFaninC0(pObj), p->vCube1 );
          if ( fVerbose )
              printf( "Output %3d:  ESOP has %5d cubes\n", i, Vec_IntSize(vEsop1) );
  //        if ( fVerbose )
  //            Eso_ManCoverPrint( p, vEsop1 );
          Vec_PtrPush( vCover, Vec_IntDup(vEsop1) );
          nCubesUsed += Vec_IntSize(vEsop1);
      }
      if ( fVerbose )
      {
          printf( "Outs = %d.  Cubes = %d.  Used = %d.  Hashed = %d. ", 
              Gia_ManCoNum(pGia), nCubes, nCubesUsed, Hsh_VecSize(p->pHash) );
          Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
      }
      if ( pvRes )
          *pvRes = Eso_ManCoverDerive( p, vCover );
      else
          pNew = Eso_ManCoverConvert( p, vCover );
      Vec_VecFree( (Vec_Vec_t *)vCover );
      Eso_ManStop( p );
      return pNew;
  }
  
  ////////////////////////////////////////////////////////////////////////
  ///                       END OF FILE                                ///
  ////////////////////////////////////////////////////////////////////////
  
  
  ABC_NAMESPACE_IMPL_END
  
  