text: /**CFile****************************************************************
  
    FileName    [extraUtilEnum.c]
  
    SystemName  [ABC: Logic synthesis and verification system.]
  
    PackageName [extra]
  
    Synopsis    [Function enumeration.]
  
    Author      [Alan Mishchenko]
    
    Affiliation [UC Berkeley]
  
    Date        [Ver. 1.0. Started - June 20, 2005.]
  
    Revision    [$Id: extraUtilEnum.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
  
  ***********************************************************************/
  
  #include <stdio.h>
  #include <stdlib.h>
  #include <string.h>
  #include <assert.h>
  #include "misc/vec/vec.h"
  #include "misc/vec/vecHsh.h"
  #include "bool/kit/kit.h"
  
  ABC_NAMESPACE_IMPL_START
  
  ////////////////////////////////////////////////////////////////////////
  ///                        DECLARATIONS                              ///
  ////////////////////////////////////////////////////////////////////////
  
  ////////////////////////////////////////////////////////////////////////
  ///                     FUNCTION DEFINITIONS                         ///
  ////////////////////////////////////////////////////////////////////////
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Abc_GetFirst( int * pnVars, int * pnMints, int * pnFuncs, unsigned * pVars, unsigned * pMints, unsigned * pFuncs )
  {
      int nVars  = 8;
      int nMints = 16;
      int nFuncs = 8;
      char * pMintStrs[16] = { 
          "1-1-1-1-",
          "1-1--11-",
          "1-1-1--1",
          "1-1--1-1",
  
          "-11-1-1-",
          "-11--11-",
          "-11-1--1",
          "-11--1-1",
  
          "1--11-1-",
          "1--1-11-",
          "1--11--1",
          "1--1-1-1",
  
          "-1-11-1-",
          "-1-1-11-",
          "-1-11--1",
          "-1-1-1-1"
      };
      char * pFuncStrs[8] = { 
          "1111101011111010",
          "0000010100000101",
          "1111110010101001",
          "0000001101010110",
          "1111111111001101",
          "0000000000110010",
          "1111111111111110",
          "0000000000000001",
      };
      int i, k;
      *pnVars  = nVars;
      *pnMints = nMints;
      *pnFuncs = nFuncs;
      // extract mints
      for ( i = 0; i < nMints; i++ )
          for ( k = 0; k < nVars; k++ )
              if ( pMintStrs[i][k] == '1' )
                  pMints[i] |= (1 << k), pVars[k] |= (1 << i);
      // extract funcs
      for ( i = 0; i < nFuncs; i++ )
          for ( k = 0; k < nMints; k++ )
              if ( pFuncStrs[i][k] == '1' )
                  pFuncs[i] |= (1 << k);
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Abc_GetSecond( int * pnVars, int * pnMints, int * pnFuncs, unsigned * pVars, unsigned * pMints, unsigned * pFuncs )
  {
      int nVars  = 10;
      int nMints = 32;
      int nFuncs = 7;
      char * pMintStrs[32] = { 
          "1-1---1---",
          "1-1----1--",
          "1-1-----1-",
          "1-1------1",
  
          "1--1--1---",
          "1--1---1--",
          "1--1----1-",
          "1--1-----1",
  
          "1---1-1---",
          "1---1--1--",
          "1---1---1-",
          "1---1----1",
  
          "1----11---",
          "1----1-1--",
          "1----1--1-",
          "1----1---1",
  
  
          "-11---1---",
          "-11----1--",
          "-11-----1-",
          "-11------1",
  
          "-1-1--1---",
          "-1-1---1--",
          "-1-1----1-",
          "-1-1-----1",
  
          "-1--1-1---",
          "-1--1--1--",
          "-1--1---1-",
          "-1--1----1",
  
          "-1---11---",
          "-1---1-1--",
          "-1---1--1-",
          "-1---1---1"
      };
      char * pFuncStrs[7] = { 
          "11111110110010001110110010000000",
          "00000001001101110001001101111111",
          "10000001001001000001001001001000",
          "01001000000100101000000100100100",
          "00100100100000010100100000010010",
          "00010010010010000010010010000001",
          "11111111111111111111000000000000"
      };
      int i, k;
      *pnVars  = nVars;
      *pnMints = nMints;
      *pnFuncs = nFuncs;
      // extract mints
      for ( i = 0; i < nMints; i++ )
          for ( k = 0; k < nVars; k++ )
              if ( pMintStrs[i][k] == '1' )
                  pMints[i] |= (1 << k), pVars[k] |= (1 << i);
      // extract funcs
      for ( i = 0; i < nFuncs; i++ )
          for ( k = 0; k < nMints; k++ )
              if ( pFuncStrs[i][k] == '1' )
                  pFuncs[i] |= (1 << k);
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Abc_GetThird( int * pnVars, int * pnMints, int * pnFuncs, unsigned * pVars, unsigned * pMints, unsigned * pFuncs )
  {
      int nVars  = 8;
      int nMints = 16;
      int nFuncs = 7;
      char * pMintStrs[16] = { 
          "1---1---",
          "1----1--",
          "1-----1-",
          "1------1",
  
          "-1--1---",
          "-1---1--",
          "-1----1-",
          "-1-----1",
  
          "--1-1---",
          "--1--1--",
          "--1---1-",
          "--1----1",
  
          "---11---",
          "---1-1--",
          "---1--1-",
          "---1---1"
      };
      char * pFuncStrs[7] = { 
          "1111111011001000",
          "0000000100110111",
          "1000000100100100",
          "0100100000010010",
          "0010010010000001",
          "0001001001001000",
          "1111111111111111"
      };
      int i, k;
      *pnVars  = nVars;
      *pnMints = nMints;
      *pnFuncs = nFuncs;
      // extract mints
      for ( i = 0; i < nMints; i++ )
          for ( k = 0; k < nVars; k++ )
              if ( pMintStrs[i][k] == '1' )
                  pMints[i] |= (1 << k), pVars[k] |= (1 << i);
      // extract funcs
      for ( i = 0; i < nFuncs; i++ )
          for ( k = 0; k < nMints; k++ )
              if ( pFuncStrs[i][k] == '1' )
                  pFuncs[i] |= (1 << k);
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Abc_EnumPrint_rec( Vec_Int_t * vGates, int i, int nVars )
  {
      int Fan0 = Vec_IntEntry(vGates, 2*i);
      int Fan1 = Vec_IntEntry(vGates, 2*i+1);
      char * pOper = (char*)(Fan0 < Fan1 ? "" : "+");
      if ( Fan0 > Fan1 )
          ABC_SWAP( int, Fan0, Fan1 );
      if ( Fan0 < nVars )
          printf( "%c", 'a'+Fan0 );
      else
      {
          printf( "(" );
          Abc_EnumPrint_rec( vGates, Fan0, nVars );
          printf( ")" );
      }
      printf( "%s", pOper );
      if ( Fan1 < nVars )
          printf( "%c", 'a'+Fan1 );
      else
      {
          printf( "(" );
          Abc_EnumPrint_rec( vGates, Fan1, nVars );
          printf( ")" );
      }
  }
  void Abc_EnumPrint( Vec_Int_t * vGates, int i, int nVars )
  {
      assert( 2*i < Vec_IntSize(vGates) );
      Abc_EnumPrint_rec( vGates, i, nVars );
      printf( "\n" );
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  static inline int  Abc_DataHasBit( word * p, word i )  { return (p[(i)>>6] & (((word)1)<<((i) & 63))) > 0; }
  static inline void Abc_DataXorBit( word * p, word i )  { p[(i)>>6] ^= (((word)1)<<((i) & 63));             }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Abc_EnumerateFunctions( int nDecMax )
  {
      int nVars;
      int nMints;
      int nFuncs;
      unsigned pVars[100] = {0};
      unsigned pMints[100] = {0};
      unsigned pFuncs[100] = {0};
      unsigned Truth;
      int FuncDone[100] = {0}, nFuncDone = 0;
      int GateCount[100] = {0};
      int i, k, n, a, b, v;
      abctime clk = Abc_Clock();
      Vec_Int_t * vGates = Vec_IntAlloc( 100000 );
      Vec_Int_t * vTruths = Vec_IntAlloc( 100000 );
  //    Vec_Int_t * vHash = Vec_IntStartFull( 1 << 16 );
      word * pHash;
  
      // extract data
  //    Abc_GetFirst( &nVars, &nMints, &nFuncs, pVars, pMints, pFuncs );
      Abc_GetSecond( &nVars, &nMints, &nFuncs, pVars, pMints, pFuncs );
  //    Abc_GetThird( &nVars, &nMints, &nFuncs, pVars, pMints, pFuncs );
  
      // create hash table
      assert( nMints == 16 || nMints == 32 );
      pHash = (word *)ABC_CALLOC( char, 1 << (nMints-3) );
  
      // create elementary gates
      for ( k = 0; k < nVars; k++ )
      {
  //        Vec_IntWriteEntry( vHash, pVars[k], k );
          Abc_DataXorBit( pHash, pVars[k] );
          Vec_IntPush( vTruths, pVars[k] );
          Vec_IntPush( vGates, -1 );
          Vec_IntPush( vGates, -1 );
      }
  
      // go through different number of variables
      GateCount[0] = 0;
      GateCount[1] = nVars;
      assert( Vec_IntSize(vTruths) == nVars );
      for ( n = 0; n < nDecMax && nFuncDone < nFuncs; n++ )
      {
          for ( a = 0; a <= n; a++ )
          for ( b = a; b <= n; b++ )
          if ( a + b == n )
          {
              printf( "Trying %d + %d + 1 = %d\n", a, b, n+1 );
              for ( i = GateCount[a]; i < GateCount[a+1]; i++ )
              for ( k = GateCount[b]; k < GateCount[b+1]; k++ )
              if ( i < k )
              {
                  Truth = Vec_IntEntry(vTruths, i) & Vec_IntEntry(vTruths, k);
  //                if ( Vec_IntEntry(vHash, Truth) == -1 )
                  if ( !Abc_DataHasBit(pHash, Truth) )
                  {
  //                    Vec_IntWriteEntry( vHash, Truth, Vec_IntSize(vTruths) );
                      Abc_DataXorBit( pHash, Truth );
                      Vec_IntPush( vTruths, Truth );
                      Vec_IntPush( vGates, i );
                      Vec_IntPush( vGates, k );
  
                      for ( v = 0; v < nFuncs; v++ )
                      if ( !FuncDone[v] && Truth == pFuncs[v] )
                      {
                          printf( "Found function %d with %d gates: ", v, n+1 );
                          Abc_EnumPrint( vGates, Vec_IntSize(vTruths)-1, nVars );
                          FuncDone[v] = 1;
                          nFuncDone++;
                      }
                  }
                  Truth = Vec_IntEntry(vTruths, i) | Vec_IntEntry(vTruths, k);
  //                if ( Vec_IntEntry(vHash, Truth) == -1 )
                  if ( !Abc_DataHasBit(pHash, Truth) )
                  {
  //                    Vec_IntWriteEntry( vHash, Truth, Vec_IntSize(vTruths) );
                      Abc_DataXorBit( pHash, Truth );
                      Vec_IntPush( vTruths, Truth );
                      Vec_IntPush( vGates, k );
                      Vec_IntPush( vGates, i );
  
                      for ( v = 0; v < nFuncs; v++ )
                      if ( !FuncDone[v] && Truth == pFuncs[v] )
                      {
                          printf( "Found function %d with %d gates: ", v, n+1 );
                          Abc_EnumPrint( vGates, Vec_IntSize(vTruths)-1, nVars );
                          FuncDone[v] = 1;
                          nFuncDone++;
                      }
                  }
              }
          }
          GateCount[n+2] = Vec_IntSize(vTruths);
          printf( "Finished %d gates.  Truths = %10d.  ", n+1, Vec_IntSize(vTruths) );
          Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
      }
      ABC_FREE( pHash );
  //    Vec_IntFree( vHash );
      Vec_IntFree( vGates );
      Vec_IntFree( vTruths );
  }
  
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  #define ABC_ENUM_MAX 16
  static word s_Truths6[6] = {
      ABC_CONST(0xAAAAAAAAAAAAAAAA),
      ABC_CONST(0xCCCCCCCCCCCCCCCC),
      ABC_CONST(0xF0F0F0F0F0F0F0F0),
      ABC_CONST(0xFF00FF00FF00FF00),
      ABC_CONST(0xFFFF0000FFFF0000),
      ABC_CONST(0xFFFFFFFF00000000)
  };
  typedef struct Abc_EnuMan_t_ Abc_EnuMan_t;
  struct Abc_EnuMan_t_
  {
      int              nVars;        // support size
      int              nVarsFree;    // number of PIs used
      int              fVerbose;     // verbose flag
      int              fUseXor;      // using XOR gate
      int              nNodeMax;     // the max number of nodes
      int              nNodes;       // current number of gates
      int              nTops;        // the number of fanoutless gates
      int              pFans0[ABC_ENUM_MAX];   // fanins
      int              pFans1[ABC_ENUM_MAX];   // fanins 
      int              fCompl0[ABC_ENUM_MAX];  // complements
      int              fCompl1[ABC_ENUM_MAX];  // complements
      int              Polar[ABC_ENUM_MAX];    // polarity
      int              pRefs[ABC_ENUM_MAX];    // references
      int              pLevel[ABC_ENUM_MAX];   // level 
      word             pTruths[ABC_ENUM_MAX];  // truth tables
      word             nTries;       // attempts to build a gate
      word             nBuilds;      // actually built gates
      word             nFinished;    // finished structures
  };
  static inline void Abc_EnumRef( Abc_EnuMan_t * p, int i )
  {
      assert( p->pRefs[i] >= 0 );
      if ( p->pRefs[i]++ == 0 )
          p->nTops--;
  }
  static inline void Abc_EnumDeref( Abc_EnuMan_t * p, int i )
  {
      if ( --p->pRefs[i] == 0 )
          p->nTops++;
      assert( p->pRefs[i] >= 0 );
  }
  static inline void Abc_EnumRefNode( Abc_EnuMan_t * p, int i )
  {
      Abc_EnumRef( p, p->pFans0[i] );
      Abc_EnumRef( p, p->pFans1[i] );
      p->nTops++;
      p->nNodes++; 
      assert( i < p->nNodes );
  }
  static inline void Abc_EnumDerefNode( Abc_EnuMan_t * p, int i )
  {
      assert( i < p->nNodes );
      Abc_EnumDeref( p, p->pFans0[i] );
      Abc_EnumDeref( p, p->pFans1[i] );
      p->nTops--;
      p->nNodes--; 
  }
  static inline void Abc_EnumPrintOne( Abc_EnuMan_t * p )
  {
      int i;
      Kit_DsdPrintFromTruth( (unsigned *)(p->pTruths + p->nNodes - 1), p->nVars ); 
      for ( i = p->nVars; i < p->nNodes; i++ )
          if ( p->Polar[i] == 4 )
              printf( "  %c=%c+%c", 'a'+i, 'a'+p->pFans0[i], 'a'+p->pFans1[i] );
          else
              printf( "  %c=%s%c%s%c", 'a'+i, p->fCompl0[i]?"!":"", 'a'+p->pFans0[i], p->fCompl1[i]?"!":"", 'a'+p->pFans1[i] );
      printf( "\n" );
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  static inline int Abc_EnumEquiv( word a, word b )
  {
      return a == b || a == ~b;
  }
  static inline int Abc_EnumerateFilter( Abc_EnuMan_t * p )
  {
      int fUseFull = 1;
      int n = p->nNodes;
      int i = p->pFans0[n];
      int k = p->pFans1[n], t;
      word * pTruths = p->pTruths;
      word uTruth = pTruths[n];
      assert( i < k );
      // skip constants
      if ( Abc_EnumEquiv(uTruth, 0) )
          return 1;
      // skip equal ones
      for ( t = 0; t < n; t++ )
          if ( Abc_EnumEquiv(uTruth, pTruths[t]) )
              return 1;
      if ( fUseFull )
      {
          // skip those that can be derived by any pair
          int a, b; 
          for ( a = 0; a <= i; a++ )
          for ( b = a + 1; b <= k; b++ )
          {
              if ( a == i && b == k )
                  continue;
              if ( Abc_EnumEquiv(uTruth,  pTruths[a] &  pTruths[b]) )
                  return 1;
              if ( Abc_EnumEquiv(uTruth,  pTruths[a] & ~pTruths[b]) )
                  return 1;
              if ( Abc_EnumEquiv(uTruth, ~pTruths[a] &  pTruths[b]) )
                  return 1;
              if ( Abc_EnumEquiv(uTruth, ~pTruths[a] & ~pTruths[b]) )
                  return 1;
              if ( p->fUseXor && Abc_EnumEquiv(uTruth,  pTruths[a] ^ pTruths[b]) )
                  return 1;
          }
      }
      else
      {
          // skip those that can be derived by fanin and any other one in the cone
          int uTruthI = p->fCompl0[n] ? ~pTruths[i] : pTruths[i];
          int uTruthK = p->fCompl1[n] ? ~pTruths[k] : pTruths[k];
          assert( p->fUseXor == 0 );
          for ( t = 0; t < k; t++ )
              if ( Abc_EnumEquiv(uTruth, pTruths[t] & uTruthI) || Abc_EnumEquiv(uTruth, ~pTruths[t] & uTruthI) )
                  return 1;
          for ( t = 0; t < i; t++ )
              if ( Abc_EnumEquiv(uTruth, pTruths[t] & uTruthK) || Abc_EnumEquiv(uTruth, ~pTruths[t] & uTruthK) )
                  return 1;
      }
      return 0;
  }
  void Abc_EnumerateFuncs_rec( Abc_EnuMan_t * p, int fNew, int iNode1st ) // the first node on the last level
  {
      if ( p->nNodes == p->nNodeMax )
      {
          assert( p->nTops == 1 );
          if ( p->fVerbose )
              Abc_EnumPrintOne( p );
          p->nFinished++;
          return;
      }
      {
      int i, k, c, cLim = 4 + p->fUseXor, n = p->nNodes;
      int nRefedFans = p->nNodeMax - n + 1 - p->nTops;
      int high0 = fNew ? iNode1st : p->pFans1[n-1];
      int high1 = fNew ? n        : iNode1st;
      int low0  = fNew ? 0        : p->pFans0[n-1];
      int c0    = fNew ? 0        : p->Polar[n-1];
      int Level = p->pLevel[high0];
      assert( p->nTops > 0 && p->nTops <= p->nNodeMax - n + 1 );
      // go through nodes 
      for ( k = high0; k < high1; k++ )
      {
          if ( nRefedFans == 0 && p->pRefs[k] > 0 )
              continue;
          if ( p->pRefs[k] > 0 )
              nRefedFans--;
          assert( nRefedFans >= 0 );
          // try second fanin
          for ( i = (k == high0) ? low0 : 0; i < k; i++ )
          {
              if ( nRefedFans == 0 && p->pRefs[i] > 0 )
                  continue;
              if ( Level == 0 && p->pRefs[i] == 0 && p->pRefs[k] == 0 && (i+1 != k || (i > 0 && p->pRefs[i-1] == 0)) ) // NPN
                  continue;
              if ( p->pLevel[k] == 0 && p->pRefs[k] == 0 && p->pRefs[i] != 0 && k > 0 && p->pRefs[k-1] == 0 ) // NPN
                  continue;
  //            if ( p->pLevel[i] == 0 && p->pRefs[i] == 0 && p->pRefs[k] != 0 && i > 0 && p->pRefs[i-1] == 0 ) // NPN
  //                continue;
              // try four polarities
              for ( c = (k == high0 && i == low0 && !fNew) ? c0 + 1 : 0; c < cLim; c++ )
              {
                  if ( p->pLevel[i] == 0 && p->pRefs[i] == 0 && (c & 1) == 1 ) // NPN
                      continue;
                  if ( p->pLevel[k] == 0 && p->pRefs[k] == 0 && (c & 2) == 2 ) // NPN
                      continue;
                  p->nTries++;
                  // create node
                  assert( i < k );
                  p->pFans0[n]  = i;
                  p->pFans1[n]  = k;
                  p->fCompl0[n] = c & 1;
                  p->fCompl1[n] = (c >> 1) & 1;
                  p->Polar[n]   = c;
                  if ( c == 4 )
                      p->pTruths[n] = p->pTruths[i] ^ p->pTruths[k];
                  else
                      p->pTruths[n] = ((c & 1) ? ~p->pTruths[i] : p->pTruths[i]) & ((c & 2) ? ~p->pTruths[k] : p->pTruths[k]);
                  if ( Abc_EnumerateFilter(p) )
                      continue;
                  p->nBuilds++;
                  assert( Level == Abc_MaxInt(p->pLevel[i], p->pLevel[k]) );
                  p->pLevel[n]  = Level + 1;
                  Abc_EnumRefNode( p, n );
                  Abc_EnumerateFuncs_rec( p, 0, fNew ? n : iNode1st );
                  Abc_EnumDerefNode( p, n );
                  assert( n == p->nNodes );
              }
          }
          if ( p->pRefs[k] > 0 )
              nRefedFans++;
      }
      if ( fNew )
          return;
      // start a new level
      Abc_EnumerateFuncs_rec( p, 1, iNode1st );
      }
  }
  void Abc_EnumerateFuncs( int nVars, int nGates, int fVerbose )
  {
      abctime clk = Abc_Clock();
      Abc_EnuMan_t P, * p = &P; 
      int i;
      if ( nVars > nGates + 1 )
      {
          printf( "The gate count %d is not enough to have functions with %d inputs.\n", nGates, nVars );
          return;
      }
      assert( nVars >= 2 && nVars <= 6 );
      assert( nGates > 0 && nVars + nGates < ABC_ENUM_MAX );
      memset( p, 0, sizeof(Abc_EnuMan_t) );
      p->fVerbose  = fVerbose;
      p->fUseXor   = 0;
      p->nVars     = nVars;
      p->nNodeMax  = nVars + nGates;
      p->nNodes    = nVars;
      p->nTops     = nVars;
      for ( i = 0; i < nVars; i++ )
          p->pTruths[i] = s_Truths6[i];
      Abc_EnumerateFuncs_rec( p, 1, 0 );
      assert( p->nNodes == nVars );
      assert( p->nTops == nVars );
      // report statistics
      printf( "Vars = %d.  Gates = %d.  Tries = %u. Builds = %u.  Finished = %d. ", 
          nVars, nGates, (unsigned)p->nTries, (unsigned)p->nBuilds, (unsigned)p->nFinished );
      Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
  }
  
  ////////////////////////////////////////////////////////////////////////
  ///                       END OF FILE                                ///
  ////////////////////////////////////////////////////////////////////////
  
  
  ABC_NAMESPACE_IMPL_END
  
  