text: #include <stdio.h>
  #include "base/main/main.h"
  #include "aig/aig/aig.h"
  #include "aig/saig/saig.h"
  #include <string.h>
  #include "base/main/mainInt.h"
  #include "proof/pdr/pdr.h"
  #include <time.h>
  
  ABC_NAMESPACE_IMPL_START
  
  long countCombination(long n, long k)
  {
      assert( n >= k );
      if( n == k ) return 1;
      if( k == 1 ) return n;
      return countCombination( n-1, k-1 ) + countCombination( n-1, k );
  }    
  
  void listCombination(int n, int t)
  {
      Vec_Int_t *vC;
      int i, j, combCounter = 0;
  
      //Initialization
      vC = Vec_IntAlloc(t+3);
      for(i=-1; i<t; i++)
          Vec_IntPush( vC, i );
      Vec_IntPush( vC, n );
      Vec_IntPush( vC, 0 );
  
      while(1)
      {
          //visit combination
          printf("Comb-%3d : ", ++combCounter);
          for( i=t; i>0; i--)
              printf("vC[%d] = %d ", i, Vec_IntEntry(vC, i));
          printf("\n");
  
          j = 1;
          while( Vec_IntEntry( vC, j ) + 1 == Vec_IntEntry( vC, j+1 ) )
          {
              //printf("\nGochon = %d, %d\n", Vec_IntEntry( vC, j ) + 1, Vec_IntEntry( vC, j+1 ));
              Vec_IntWriteEntry( vC, j, j-1 );
              j = j + 1;
          }
          if( j > t ) break;
          Vec_IntWriteEntry( vC, j, Vec_IntEntry( vC, j ) + 1 );
      }
      
      Vec_IntFree(vC);    
  }
  
  int generateCombinatorialStabil( Aig_Man_t *pAigNew, Aig_Man_t *pAigOld, 
                  Vec_Int_t *vCandidateMonotoneSignals_,
                  Vec_Ptr_t *vDisj_nCk_,
                  int combN, int combK )
  {
      Aig_Obj_t *pObjMonoCand, *pObj;
      int targetPoIndex;
  
      //Knuth's Data Strcuture
      int totalCombination_KNUTH = 0;
      Vec_Int_t *vC_KNUTH;
      int i_KNUTH, j_KNUTH;
  
      //Knuth's Data Structure Initialization
      vC_KNUTH = Vec_IntAlloc(combK+3);
      for(i_KNUTH=-1; i_KNUTH<combK; i_KNUTH++)
          Vec_IntPush( vC_KNUTH, i_KNUTH );
      Vec_IntPush( vC_KNUTH, combN );
      Vec_IntPush( vC_KNUTH, 0 );
  
      while(1)
      {
          totalCombination_KNUTH++;
          pObjMonoCand = Aig_Not(Aig_ManConst1(pAigNew));
          for( i_KNUTH=combK; i_KNUTH>0; i_KNUTH--)
          {
              targetPoIndex = Vec_IntEntry( vCandidateMonotoneSignals_, Vec_IntEntry(vC_KNUTH, i_KNUTH));
              pObj = Aig_ObjChild0Copy(Aig_ManCo( pAigOld, targetPoIndex ));
              pObjMonoCand = Aig_Or( pAigNew, pObj, pObjMonoCand );
          }
          Vec_PtrPush(vDisj_nCk_, pObjMonoCand );
  
          j_KNUTH = 1;
          while( Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 == Vec_IntEntry( vC_KNUTH, j_KNUTH+1 ) )
          {
              Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, j_KNUTH-1 );
              j_KNUTH = j_KNUTH + 1;
          }
          if( j_KNUTH > combK ) break;
          Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 );
      }
  
      Vec_IntFree(vC_KNUTH);
  
      return totalCombination_KNUTH;
  }
  
  int generateCombinatorialStabilExhaust( Aig_Man_t *pAigNew, Aig_Man_t *pAigOld, 
                  Vec_Ptr_t *vDisj_nCk_,
                  int combN, int combK )
  {
      Aig_Obj_t *pObjMonoCand, *pObj;
      int targetPoIndex;
  
      //Knuth's Data Strcuture
      int totalCombination_KNUTH = 0;
      Vec_Int_t *vC_KNUTH;
      int i_KNUTH, j_KNUTH;
  
      //Knuth's Data Structure Initialization
      vC_KNUTH = Vec_IntAlloc(combK+3);
      for(i_KNUTH=-1; i_KNUTH<combK; i_KNUTH++)
          Vec_IntPush( vC_KNUTH, i_KNUTH );
      Vec_IntPush( vC_KNUTH, combN );
      Vec_IntPush( vC_KNUTH, 0 );
  
      while(1)
      {
          totalCombination_KNUTH++;
          pObjMonoCand = Aig_Not(Aig_ManConst1(pAigNew));
          for( i_KNUTH=combK; i_KNUTH>0; i_KNUTH--)
          {
              //targetPoIndex = Vec_IntEntry( vCandidateMonotoneSignals_, Vec_IntEntry(vC_KNUTH, i_KNUTH));
              targetPoIndex = Vec_IntEntry(vC_KNUTH, i_KNUTH);
              pObj = (Aig_Obj_t *)(Aig_ManLo( pAigOld, targetPoIndex )->pData);
              pObjMonoCand = Aig_Or( pAigNew, pObj, pObjMonoCand );
          }
          Vec_PtrPush(vDisj_nCk_, pObjMonoCand );
  
          j_KNUTH = 1;
          while( Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 == Vec_IntEntry( vC_KNUTH, j_KNUTH+1 ) )
          {
              Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, j_KNUTH-1 );
              j_KNUTH = j_KNUTH + 1;
          }
          if( j_KNUTH > combK ) break;
          Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 );
      }
  
      Vec_IntFree(vC_KNUTH);
  
      return totalCombination_KNUTH;
  }
  
  Aig_Man_t *generateDisjunctiveTester( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combN, int combK )
  {
      //AIG creation related data structure
      Aig_Man_t *pNewAig;
      int piCopied = 0, loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0, poCopied = 0;
      //int i, iElem, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker;
      int i, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker;
      int combN_internal, combK_internal; //, targetPoIndex;
      long longI, lCombinationCount;
      //Aig_Obj_t *pObj, *pObjMonoCand, *pObjLO_nCk, *pObjDisj_nCk;
      Aig_Obj_t *pObj, *pObjLO_nCk, *pObjDisj_nCk;
      Vec_Ptr_t *vLO_nCk, *vPODriver_nCk, *vDisj_nCk;
      Vec_Int_t *vCandidateMonotoneSignals;
  
      extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk);
      
      //Knuth's Data Strcuture
      //Vec_Int_t *vC_KNUTH;
      //int i_KNUTH, j_KNUTH, combCounter_KNUTH = 0;
  
      //Collecting target HINT signals
      vCandidateMonotoneSignals = findHintOutputs(pNtk);
      if( vCandidateMonotoneSignals == NULL )
      {
          printf("\nTraget Signal Set is Empty: Duplicating given AIG\n");
          combN_internal = 0;
      }
      else
      {
          //Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
          //    printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
          hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
          hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
          combN_internal = hintSingalEndMarker - hintSingalBeginningMarker + 1;
      }
  
      //combK_internal = combK;
  
      //Knuth's Data Structure Initialization
      //vC_KNUTH = Vec_IntAlloc(combK_internal+3);
      //for(i_KNUTH=-1; i_KNUTH<combK_internal; i_KNUTH++)
      //    Vec_IntPush( vC_KNUTH, i_KNUTH );
      //Vec_IntPush( vC_KNUTH, combN_internal );
      //Vec_IntPush( vC_KNUTH, 0 );
  
      //Standard AIG duplication begins
      //Standard AIG Manager Creation
      pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
      pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_nCk") + 1 );
      sprintf(pNewAig->pName, "%s_%s", pAig->pName, "nCk");
          pNewAig->pSpec = NULL;
  
      //Standard Mapping of Constant Nodes
      pObj = Aig_ManConst1( pAig );
          pObj->pData = Aig_ManConst1( pNewAig );
  
      //Standard AIG PI duplication
      Saig_ManForEachPi( pAig, pObj, i )
      {
          piCopied++;
          pObj->pData = Aig_ObjCreateCi(pNewAig);
      }
  
      //Standard AIG LO duplication
      Saig_ManForEachLo( pAig, pObj, i )
          {
          loCopied++;
          pObj->pData = Aig_ObjCreateCi(pNewAig);
          }
  
      //nCk LO creation
      lCombinationCount = 0;
      for(combK_internal=1; combK_internal<=combK; combK_internal++)
          lCombinationCount += countCombination( combN_internal, combK_internal );
      assert( lCombinationCount > 0 );
      vLO_nCk = Vec_PtrAlloc(lCombinationCount);
      for( longI = 0; longI < lCombinationCount; longI++ )
      {
          loCreated++;
          pObj = Aig_ObjCreateCi(pNewAig);
          Vec_PtrPush( vLO_nCk, pObj );
      }
  
      //Standard Node duplication
      Aig_ManForEachNode( pAig, pObj, i )
      {
          pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
      }
      
      //nCk specific logic creation (i.e. nCk number of OR gates)
      vDisj_nCk = Vec_PtrAlloc(lCombinationCount);
  
      
  
      //while(1)
      //{
      //    //visit combination
      //    //printf("Comb-%3d : ", ++combCounter_KNUTH);
      //    pObjMonoCand = Aig_Not(Aig_ManConst1(pNewAig));
      //    for( i_KNUTH=combK_internal; i_KNUTH>0; i_KNUTH--)
      //    {
      //        //printf("vC[%d] = %d ", i_KNUTH, Vec_IntEntry(vC_KNUTH, i_KNUTH));
      //        targetPoIndex = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntEntry(vC_KNUTH, i_KNUTH));
      //        pObj = Aig_ObjChild0Copy(Aig_ManCo( pAig, targetPoIndex ));
      //        pObjMonoCand = Aig_Or( pNewAig, pObj, pObjMonoCand );
      //    }
      //    Vec_PtrPush(vDisj_nCk, pObjMonoCand );
      //    //printf("\n");
  
      //    j_KNUTH = 1;
      //    while( Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 == Vec_IntEntry( vC_KNUTH, j_KNUTH+1 ) )
      //    {
      //        Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, j_KNUTH-1 );
      //        j_KNUTH = j_KNUTH + 1;
      //    }
      //    if( j_KNUTH > combK_internal ) break;
      //    Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 );
      //}
      for( combK_internal=1; combK_internal<=combK; combK_internal++ )
          generateCombinatorialStabil( pNewAig, pAig, vCandidateMonotoneSignals,
                  vDisj_nCk, combN_internal, combK_internal );
  
  
      //creation of implication logic
      vPODriver_nCk = Vec_PtrAlloc(lCombinationCount);
      for( longI = 0; longI < lCombinationCount; longI++ )
      {
          pObjLO_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vLO_nCk, longI ));
          pObjDisj_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vDisj_nCk, longI ));
  
          pObj = Aig_Or( pNewAig, Aig_Not(pObjDisj_nCk), pObjLO_nCk);
          Vec_PtrPush(vPODriver_nCk, pObj);
      }
      
      //Standard PO duplication
      Saig_ManForEachPo( pAig, pObj, i )
      {
          poCopied++;
          pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
      }
  
      //nCk specific PO creation
      for( longI = 0; longI < lCombinationCount; longI++ )
      {
          Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
      }
  
      //Standard LI duplication
      Saig_ManForEachLi( pAig, pObj, i )
      {
          liCopied++;
          Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
      }
  
      //nCk specific LI creation
      for( longI = 0; longI < lCombinationCount; longI++ )
      {
          liCreated++;
          Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
      }
  
      //clean-up, book-keeping
      assert( liCopied + liCreated == loCopied + loCreated );    
      nRegCount = loCopied + loCreated;
  
      Aig_ManSetRegNum( pNewAig, nRegCount );
      Aig_ManCleanup( pNewAig );
      assert( Aig_ManCheck( pNewAig ) );
      
      //Vec_IntFree(vC_KNUTH);    
      return pNewAig;
  }
  
  Aig_Man_t *generateGeneralDisjunctiveTester( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combK )
  {
      //AIG creation related data structure
      Aig_Man_t *pNewAig;
      int piCopied = 0, loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0, poCopied = 0;
      //int i, iElem, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker;
      int i, nRegCount;
      int combN_internal, combK_internal; //, targetPoIndex;
      long longI, lCombinationCount;
      //Aig_Obj_t *pObj, *pObjMonoCand, *pObjLO_nCk, *pObjDisj_nCk;
      Aig_Obj_t *pObj, *pObjLO_nCk, *pObjDisj_nCk;
      Vec_Ptr_t *vLO_nCk, *vPODriver_nCk, *vDisj_nCk;
  
      extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk);
      
      //Knuth's Data Strcuture
      //Vec_Int_t *vC_KNUTH;
      //int i_KNUTH, j_KNUTH, combCounter_KNUTH = 0;
  
      //Collecting target HINT signals
      //vCandidateMonotoneSignals = findHintOutputs(pNtk);
      //if( vCandidateMonotoneSignals == NULL )
      //{
      //    printf("\nTraget Signal Set is Empty: Duplicating given AIG\n");
      //    combN_internal = 0;
      //}
      //else
      //{
          //Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
          //    printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
      //    hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
      //    hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
      //    combN_internal = hintSingalEndMarker - hintSingalBeginningMarker + 1;
      //}
  
      combN_internal = Aig_ManRegNum(pAig);
  
      pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
      pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_nCk") + 1 );
      sprintf(pNewAig->pName, "%s_%s", pAig->pName, "nCk");
          pNewAig->pSpec = NULL;
  
      //Standard Mapping of Constant Nodes
      pObj = Aig_ManConst1( pAig );
          pObj->pData = Aig_ManConst1( pNewAig );
  
      //Standard AIG PI duplication
      Saig_ManForEachPi( pAig, pObj, i )
      {
          piCopied++;
          pObj->pData = Aig_ObjCreateCi(pNewAig);
      }
  
      //Standard AIG LO duplication
      Saig_ManForEachLo( pAig, pObj, i )
          {
          loCopied++;
          pObj->pData = Aig_ObjCreateCi(pNewAig);
          }
  
      //nCk LO creation
      lCombinationCount = 0;
      for(combK_internal=1; combK_internal<=combK; combK_internal++)
          lCombinationCount += countCombination( combN_internal, combK_internal );
      assert( lCombinationCount > 0 );
      vLO_nCk = Vec_PtrAlloc(lCombinationCount);
      for( longI = 0; longI < lCombinationCount; longI++ )
      {
          loCreated++;
          pObj = Aig_ObjCreateCi(pNewAig);
          Vec_PtrPush( vLO_nCk, pObj );
      }
  
      //Standard Node duplication
      Aig_ManForEachNode( pAig, pObj, i )
      {
          pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
      }
      
      //nCk specific logic creation (i.e. nCk number of OR gates)
      vDisj_nCk = Vec_PtrAlloc(lCombinationCount);
  
      for( combK_internal=1; combK_internal<=combK; combK_internal++ )
      {
          generateCombinatorialStabilExhaust( pNewAig, pAig,
                  vDisj_nCk, combN_internal, combK_internal );
      }
  
  
      //creation of implication logic
      vPODriver_nCk = Vec_PtrAlloc(lCombinationCount);
      for( longI = 0; longI < lCombinationCount; longI++ )
      {
          pObjLO_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vLO_nCk, longI ));
          pObjDisj_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vDisj_nCk, longI ));
  
          pObj = Aig_Or( pNewAig, Aig_Not(pObjDisj_nCk), pObjLO_nCk);
          Vec_PtrPush(vPODriver_nCk, pObj);
      }
      
      //Standard PO duplication
      Saig_ManForEachPo( pAig, pObj, i )
      {
          poCopied++;
          pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
      }
  
      //nCk specific PO creation
      for( longI = 0; longI < lCombinationCount; longI++ )
      {
          Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
      }
  
      //Standard LI duplication
      Saig_ManForEachLi( pAig, pObj, i )
      {
          liCopied++;
          Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
      }
  
      //nCk specific LI creation
      for( longI = 0; longI < lCombinationCount; longI++ )
      {
          liCreated++;
          Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
      }
  
      //clean-up, book-keeping
      assert( liCopied + liCreated == loCopied + loCreated );    
      nRegCount = loCopied + loCreated;
  
      Aig_ManSetRegNum( pNewAig, nRegCount );
      Aig_ManCleanup( pNewAig );
      assert( Aig_ManCheck( pNewAig ) );
      
      Vec_PtrFree(vLO_nCk);
      Vec_PtrFree(vPODriver_nCk);
      Vec_PtrFree(vDisj_nCk);
      //Vec_IntFree(vC_KNUTH);    
      return pNewAig;
  }
  
  ABC_NAMESPACE_IMPL_END
  