/**CFile****************************************************************

  FileName    [lucky.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Semi-canonical form computation package.]

  Synopsis    [Truth table minimization procedures.]

  Author      [Jake]

  Date        [Started - August 2012]

***********************************************************************/

#include "luckyInt.h"

ABC_NAMESPACE_IMPL_START


int memCompare(word* x, word*  y, int nVars)
{
    int i;
    for(i=Kit_TruthWordNum_64bit( nVars )-1;i>=0;i--)
    {
        if(x[i]==y[i])
            continue;
        else if(x[i]>y[i])
            return 1;
        else
            return -1;
    }
    return 0;
}
///////sort Word* a///////////////////////////////////////////////////////////////////////////////////////////////////////
 int compareWords1 (const void * a, const void * b)
 {
     if( *(word*)a > *(word*)b )
         return 1;
     else
         return( *(word*)a < *(word*)b ) ? -1: 0;
     
 }
 
 void sortAndUnique1(word* a, Abc_TtStore_t* p)
 {
     int i, count=1, WordsN = p->nFuncs;
     word tempWord;
     qsort(a,WordsN,sizeof(word),compareWords1);
     tempWord = a[0];
     for(i=1;i<WordsN;i++)  
         if(tempWord != a[i])
         {
             a[count] = a[i];
             tempWord = a[i];
             count++;
         }
         p->nFuncs = count;
}
//////////sort Word** a//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
int compareWords2 (const void ** x, const void ** y)
{
    
    if(**(word**)x > **(word**)y)
        return 1;
    else if(**(word**)x < **(word**)y)
        return -1;
    else
        return 0;   
    
}
int compareWords (const void ** a, const void ** b)
{
     if( memcmp(*(word**)a,*(word**)b,sizeof(word)*1) > 0 )
         return 1;
     else
         return ( memcmp(*(word**)a,*(word**)b,sizeof(word)*1) < 0 ) ? -1: 0;       
}
int compareWords3 (const void ** x, const void ** y)
{
    return memCompare(*(word**)x, *(word**)y, 16);   
} 
void sortAndUnique(word** a, Abc_TtStore_t* p)
{
     int i, count=1, WordsPtrN = p->nFuncs;
     word* tempWordPtr;
     qsort(a,WordsPtrN,sizeof(word*),(int(*)(const void *,const void *))compareWords3);
     tempWordPtr = a[0];
     for(i=1;i<WordsPtrN;i++)   
         if(memcmp(a[i],tempWordPtr,sizeof(word)*(p->nWords)) != 0)
         {
             a[count] = a[i];
             tempWordPtr = a[i];
             count++;
         }
         p->nFuncs = count;
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////

typedef struct
{
     int totalCycles;
     int maxNCycles;
     int minNCycles;
     
}cycleCtr;
cycleCtr* setCycleCtrPtr()
{
     cycleCtr* x = (cycleCtr*) malloc(sizeof(cycleCtr));
     x->totalCycles=0;
     x->maxNCycles=0;
     x->minNCycles=111111111;
     return x;
}
void freeCycleCtr(cycleCtr* x)
{
    free(x);
}
word** makeArray(Abc_TtStore_t* p)
{
    int i;
    word** a;
    a = (word**)malloc(sizeof(word*)*(p->nFuncs));
    for(i=0;i<p->nFuncs;i++)
    {
        a[i] = (word*)malloc(sizeof(word)*(p->nWords));
        memcpy(a[i],p->pFuncs[i],sizeof(word)*(p->nWords));

    }
    return a;
}
void freeArray(word** a,Abc_TtStore_t* p)
{
    int i;
    for(i=0;i<p->nFuncs;i++)
        free(a[i]);
    free(a);
}

word* makeArrayB(word** a, int nFuncs)
{
    int i;
    word* b;
    b = (word*)malloc(sizeof(word)*(nFuncs));
    for(i=0;i<nFuncs;i++)
        b[i] = a[i][0];

    return b;
}
void freeArrayB(word* b)
{
    free(b);
}

////////////////////////////////////////////////////////////////////////////////////////

// if highest bit in F ( all ones min term ) is one => inverse 
// if pInOnt changed(minimized) by function return 1 if not 0
// int minimalInitialFlip_propper(word* pInOut, word* pDuplicat, int  nVars)
// {
//  word oneWord=1;
//  Kit_TruthCopy_64bit( pDuplicat, pInOut, nVars );
//  Kit_TruthNot_64bit( pDuplicat, nVars );
//  if( memCompare(pDuplicat,pInOut,nVars) == -1)
//  {
//      Kit_TruthCopy_64bit(pInOut, pDuplicat, nVars );
//      return 1;
//  }
//  return 0;
// }
// int minimalFlip(word* pInOut, word* pMinimal, word* PDuplicat, int  nVars) 
// {
//  int i;
//  int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
//  memcpy(pMinimal, pInOut, blockSize);
//  memcpy(PDuplicat, pInOut, blockSize);
//  for(i=0;i<nVars;i++)
//  {
//      Kit_TruthChangePhase_64bit( pInOut, nVars, i );
//      if( memCompare(pMinimal,pInOut,nVars) == 1)
//          memcpy(pMinimal, pInOut, blockSize);
//      memcpy(pInOut,PDuplicat,blockSize);
//  }
//  memcpy(pInOut,pMinimal,blockSize);
//  if(memCompare(pMinimal,PDuplicat,nVars) == 0)
//      return 0;
//  else
//      return 1;
// }
// int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int  nVars) 
// {
//  int i;  
//  int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
//  memcpy(pMinimal, pInOut, blockSize);
//  memcpy(PDuplicat, pInOut, blockSize);
//  for(i=0;i<nVars-1;i++)
//  {
//      Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
//      if(memCompare(pMinimal,pInOut,nVars) == 1)
//          memcpy(pMinimal, pInOut, blockSize);
//      memcpy(pInOut,PDuplicat,blockSize);
//  }
//  memcpy(pInOut,pMinimal,blockSize);
//  if(memCompare(pMinimal,PDuplicat,nVars) == 0)
//      return 0;
//  else
//      return 1;
// }
// 
// void luckyCanonicizer(word* pInOut, word* pAux, word* pAux1, int  nVars, cycleCtr* cCtr)
// {
//  int counter=1, cycles=0;   
//  assert( nVars <= 16 );
//  while(counter>0 )   //  && cycles < 10 if we wanna limit cycles
//  {
//      counter=0;
//      counter += minimalInitialFlip(pInOut, nVars);
//      counter += minimalFlip(pInOut, pAux, pAux1, nVars);
//      counter += minimalSwap(pInOut, pAux, pAux1, nVars);
//      cCtr->totalCycles++;
//      cycles++;
//  }
//  if(cycles < cCtr->minNCycles)
//      cCtr->minNCycles = cycles;
//  else if(cycles > cCtr->maxNCycles)
//      cCtr->maxNCycles = cycles;
// }
//  runs paralel F and ~F in luckyCanonicizer
// void luckyCanonicizer2(word* pInOut, word* pAux, word* pAux1, word* temp, int  nVars)
// {
//  int nWords = Kit_TruthWordNum_64bit( nVars );
//  int counter=1, nOnes;   
//  assert( nVars <= 16 );
//  nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
//  
//     if ( (nOnes*2 == nWords * 32) )
//     { 
//      Kit_TruthCopy_64bit( temp, pInOut, nVars );
//      Kit_TruthNot_64bit( temp, nVars );
//         luckyCanonicizer1_simple(pInOut, pAux, pAux1, nVars);
//      luckyCanonicizer1_simple(temp, pAux, pAux1, nVars);
//      if( memCompare(temp,pInOut,nVars) == -1)        
//          Kit_TruthCopy_64bit(pInOut, temp, nVars );  
//      return;     
//     }
//  while(counter>0 )   //  && cycles < 10 if we wanna limit cycles
//  {
//      counter=0;
//      counter += minimalInitialFlip_propper(pInOut, pAux, nVars);
//      counter += minimalFlip1(pInOut, pAux, pAux1, nVars);
//      counter += minimalSwap1(pInOut, pAux, pAux1, nVars);
//  }
// }
// same as luckyCanonicizer + cycleCtr stutistics 
// void luckyCanonicizer1(word* pInOut, word* pAux, word* pAux1, int  nVars, cycleCtr* cCtr)
// {
//  int counter=1, cycles=0;   
//  assert( nVars <= 16 );
//  while(counter>0 )   //  && cycles < 10 if we wanna limit cycles
//  {
//      counter=0;
//      counter += minimalInitialFlip1(pInOut, nVars);
//      counter += minimalFlip1(pInOut, pAux, pAux1, nVars);
//      counter += minimalSwap1(pInOut, pAux, pAux1, nVars);
//      cCtr->totalCycles++;
//      cycles++;
//  }
//  if(cycles < cCtr->minNCycles)
//      cCtr->minNCycles = cycles;
//  else if(cycles > cCtr->maxNCycles)
//      cCtr->maxNCycles = cycles;
// }
// luckyCanonicizer 

void printCCtrInfo(cycleCtr* cCtr, int nFuncs)
{
    printf("maxNCycles = %d\n",cCtr->maxNCycles);
    printf("minNCycles = %d\n",cCtr->minNCycles);
    printf("average NCycles = %.3f\n",cCtr->totalCycles/(double)nFuncs);
}
////////////////////////////////////////New Faster versoin/////////////////////////////////////////////////////////

// if highest bit in F ( all ones min term ) is one => inverse 
// returns: if pInOnt changed(minimized) by function return 1 if not 0
int minimalInitialFlip1(word* pInOut, int  nVars)
{
    word oneWord=1;
    if(  (pInOut[Kit_TruthWordNum_64bit( nVars ) -1]>>63) & oneWord )
    {
        Kit_TruthNot_64bit( pInOut, nVars );
        return 1;
    }
    return 0;
}

// compare F with  F1 = (F with changed phase in one of the vars).
// keeps smaller.
// same for all vars in F.
// returns: if pInOnt changed(minimized) by function return 1 if not 0
int minimalFlip1(word* pInOut, word* pMinimal, word* PDuplicat, int  nVars) 
{
    int i;
    int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
    memcpy(pMinimal, pInOut, blockSize);
    memcpy(PDuplicat, pInOut, blockSize);
    Kit_TruthChangePhase_64bit( pInOut, nVars, 0 );
    for(i=1;i<nVars;i++)
    {
        if( memCompare(pMinimal,pInOut,nVars) == 1)
        {
            memcpy(pMinimal, pInOut, blockSize);
            Kit_TruthChangePhase_64bit( pInOut, nVars, i );
        }
        else
        {
            memcpy(pInOut, pMinimal, blockSize);
            Kit_TruthChangePhase_64bit( pInOut, nVars, i );
        }
    }
    if( memCompare(pMinimal,pInOut,nVars) == -1)
        memcpy(pInOut, pMinimal, blockSize);
    if(memcmp(pInOut,PDuplicat,blockSize) == 0)
        return 0;
    else
        return 1;
}
// compare F with  F1 = (F with swapped two adjacent vars).
// keeps smaller.
// same for all vars in F.
// returns: if pInOnt changed(minimized) by function return 1 if not 0
int minimalSwap1(word* pInOut, word* pMinimal, word* PDuplicat, int  nVars) 
{
    int i;
    int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
    memcpy(pMinimal, pInOut, blockSize);
    memcpy(PDuplicat, pInOut, blockSize);
    Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, 0 );
    for(i=1;i<nVars-1;i++)
    {
        if( memCompare(pMinimal,pInOut,nVars) == 1)
        {
            memcpy(pMinimal, pInOut, blockSize);
            Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
        }
        else
        {
            memcpy(pInOut, pMinimal, blockSize);
            Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
        }
    }
    if( memCompare(pMinimal,pInOut,nVars) == -1)
        memcpy(pInOut, pMinimal, blockSize);
    if(memcmp(pInOut,PDuplicat,blockSize) == 0)
        return 0;
    else
        return 1;
}

// if highest bit in F ( all ones min term ) is one => inverse 
// returns: if pInOnt changed(minimized) by function return 1 if not 0
int minimalInitialFlip(word* pInOut, int  nVars, unsigned* p_uCanonPhase)
{
    word oneWord=1;
    if(  (pInOut[Kit_TruthWordNum_64bit( nVars ) -1]>>63) & oneWord )
    {
        Kit_TruthNot_64bit( pInOut, nVars );
        *p_uCanonPhase ^= (1 << nVars);
        return 1;
    }
    return 0;
}

// compare F with  F1 = (F with changed phase in one of the vars).
// keeps smaller.
// same for all vars in F.
// returns: if pInOnt changed(minimized) by function return 1 if not 0
int minimalFlip(word* pInOut, word* pMinimal, word* PDuplicat, int  nVars, unsigned* p_uCanonPhase)
{
    int i;
    unsigned minTemp = *p_uCanonPhase;
    int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
    memcpy(pMinimal, pInOut, blockSize);
    memcpy(PDuplicat, pInOut, blockSize);       //////////////need one more unsigned!!!!!!!!!!!!!
    Kit_TruthChangePhase_64bit( pInOut, nVars, 0 );
    *p_uCanonPhase ^= (unsigned)1;
    for(i=1;i<nVars;i++)
    {
        if( memCompare(pMinimal,pInOut,nVars) == 1)
        {
            memcpy(pMinimal, pInOut, blockSize);
            minTemp = *p_uCanonPhase;
        }
        else
        {
            memcpy(pInOut, pMinimal, blockSize);
            *p_uCanonPhase = minTemp;
        }
        Kit_TruthChangePhase_64bit( pInOut, nVars, i );
        *p_uCanonPhase ^= (1 << i);
    }
    if( memCompare(pMinimal,pInOut,nVars) == -1)
    {
        memcpy(pInOut, pMinimal, blockSize);
        *p_uCanonPhase = minTemp;
    }
    if(memcmp(pInOut,PDuplicat,blockSize) == 0) 
        return 0;
    else
        return 1;
}

// swaps iVar and iVar+1 elements in pCanonPerm ant p_uCanonPhase
void swapInfoAdjacentVars(int iVar, char * pCanonPerm, unsigned* p_uCanonPhase)
{
    char Temp = pCanonPerm[iVar];
    pCanonPerm[iVar] = pCanonPerm[iVar+1];
    pCanonPerm[iVar+1] = Temp;
    
    // if the polarity of variables is different, swap them
    if ( ((*p_uCanonPhase & (1 << iVar)) > 0) != ((*p_uCanonPhase & (1 << (iVar+1))) > 0) )
    {
        *p_uCanonPhase ^= (1 << iVar);
        *p_uCanonPhase ^= (1 << (iVar+1));
    }
            
}


// compare F with  F1 = (F with swapped two adjacent vars).
// keeps smaller.
// same for all vars in F.
// returns: if pInOnt changed(minimized) by function return 1 if not 0


/*
// this version is buggy and is fixed below
int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int  nVars, char * pCanonPerm, char * tempArray, unsigned* p_uCanonPhase) 
{
    int i;  
    int blockSizeWord = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
    int blockSizeChar = nVars *sizeof(char);
    memcpy(pMinimal, pInOut, blockSizeWord);
    memcpy(PDuplicat, pInOut, blockSizeWord);
    memcpy(tempArray, pCanonPerm, blockSizeChar);  
    Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, 0 );
    swapInfoAdjacentVars(0, pCanonPerm, p_uCanonPhase);
    for(i=1;i<nVars-1;i++)
    {
        if( memCompare(pMinimal,pInOut,nVars) == 1)
        {
            memcpy(pMinimal, pInOut, blockSizeWord);
            memcpy(tempArray, pCanonPerm, blockSizeChar);
        }
        else
        {
            memcpy(pInOut, pMinimal, blockSizeWord);
            memcpy(pCanonPerm, tempArray, blockSizeChar);   
        }
        Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
        swapInfoAdjacentVars(i, pCanonPerm, p_uCanonPhase);
    }
    if( memCompare(pMinimal,pInOut,nVars) == -1)
    {
        memcpy(pInOut, pMinimal, blockSizeWord);
        memcpy(pCanonPerm, tempArray, blockSizeChar);
    }
    if(memcmp(pInOut,PDuplicat,blockSizeWord) == 0)
        return 0;
    else
        return 1;
}
*/

int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int  nVars, char * pCanonPerm, char * tempArray, unsigned* p_uCanonPhase) 
{
    int i;  
    int blockSizeWord = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
    int blockSizeChar = nVars *sizeof(char);
    unsigned TempuCanonPhase = *p_uCanonPhase;
    memcpy(pMinimal, pInOut, blockSizeWord);
    memcpy(PDuplicat, pInOut, blockSizeWord);
    memcpy(tempArray, pCanonPerm, blockSizeChar);  
    Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, 0 );
    swapInfoAdjacentVars(0, pCanonPerm, p_uCanonPhase);
    for(i=1;i<nVars-1;i++)
    {
        if( memCompare(pMinimal,pInOut,nVars) == 1)
        {
            memcpy(pMinimal, pInOut, blockSizeWord);
            memcpy(tempArray, pCanonPerm, blockSizeChar);
            TempuCanonPhase = *p_uCanonPhase;
            
        }
        else
        {
            memcpy(pInOut, pMinimal, blockSizeWord);
            memcpy(pCanonPerm, tempArray, blockSizeChar);
            *p_uCanonPhase = TempuCanonPhase;
        }
        Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
        swapInfoAdjacentVars(i, pCanonPerm, p_uCanonPhase);
    }
    if( memCompare(pMinimal,pInOut,nVars) == -1)
    {
        memcpy(pInOut, pMinimal, blockSizeWord);
        memcpy(pCanonPerm, tempArray, blockSizeChar);
        *p_uCanonPhase = TempuCanonPhase;
    }
    if(memcmp(pInOut,PDuplicat,blockSizeWord) == 0)
        return 0;
    else
        return 1;
}


//////////////// functions below just for Alan if he want to double check my program//////////////////////////////////
/////////////////You need swap_ij function or analogical one//////////////////////////////////////////////////////////
/*
void swapAndFlip(word* pAfter, int nVars, int iVarInPosition, int jVar, char * pCanonPerm, unsigned* pUCanonPhase)
{
    int Temp;
    swap_ij(pAfter, nVars, iVarInPosition, jVar);
    
    Temp = pCanonPerm[iVarInPosition];
    pCanonPerm[iVarInPosition] = pCanonPerm[jVar];
    pCanonPerm[jVar] = Temp;
    
    if ( ((*pUCanonPhase & (1 << iVarInPosition)) > 0) != ((*pUCanonPhase & (1 << jVar)) > 0) )
    {
        *pUCanonPhase ^= (1 << iVarInPosition);
        *pUCanonPhase ^= (1 << jVar);
    }
    if(*pUCanonPhase>>iVarInPosition & (unsigned)1 == 1)
        Kit_TruthChangePhase_64bit( pAfter, nVars, iVarInPosition );
    
}
int luckyCheck(word* pAfter, word* pBefore, int nVars, char * pCanonPerm, unsigned uCanonPhase)
{
    int i,j;
    char tempChar;
    for(j=0;j<nVars;j++)
    {
        tempChar = 'a'+ j;
        for(i=j;i<nVars;i++)
        {
            if(tempChar != pCanonPerm[i])
                continue;
            swapAndFlip(pAfter , nVars, j, i, pCanonPerm, &uCanonPhase);
            break;
        }
    }
    if(uCanonPhase>>nVars & (unsigned)1 == 1)
        Kit_TruthNot_64bit(pAfter, nVars );
    if(memcmp(pAfter, pBefore, Kit_TruthWordNum_64bit( nVars )*sizeof(word)) == 0)
        return 0;
    else
        return 1;
}
*/
//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////


void luckyCanonicizer(word* pInOut, word* pAux, word* pAux1, int  nVars, char * pCanonPerm, char * tempArray, unsigned* p_uCanonPhase)
{
    int counter=1;
    assert( nVars <= 16 );
    while(counter>0 )   //  && cycles < 10 if we wanna limit cycles
    {
        counter=0;
        counter += minimalInitialFlip(pInOut, nVars, p_uCanonPhase);
        counter += minimalFlip(pInOut, pAux, pAux1, nVars, p_uCanonPhase);
        counter += minimalSwap(pInOut, pAux, pAux1, nVars, pCanonPerm, tempArray, p_uCanonPhase);   
    }
}
// tries to find minimal F till F at the beginning of the loop is the same as at the end - irreducible 
unsigned luckyCanonicizer1_simple(word* pInOut, word* pAux, word* pAux1, int  nVars, char * pCanonPerm, unsigned CanonPhase)
{
    int counter=1;
    assert( nVars <= 16 );
    while(counter>0 )   //  && cycles < 10 if we wanna limit cycles
    {
        counter=0;
        counter += minimalInitialFlip1(pInOut, nVars);
        counter += minimalFlip1(pInOut, pAux, pAux1, nVars);
        counter += minimalSwap1(pInOut, pAux, pAux1, nVars);    
    }
    return CanonPhase;
}

void luckyCanonicizer_final(word* pInOut, word* pAux, word* pAux1, int  nVars)
{
    Kit_TruthSemiCanonicize_Yasha_simple( pInOut, nVars, NULL );
    luckyCanonicizer1_simple(pInOut, pAux, pAux1, nVars, NULL, 0);
}

// this procedure calls internal canoniziers
// it returns canonical phase (as return value) and canonical permutation (in pCanonPerm)
unsigned Kit_TruthSemiCanonicize_new_internal( word * pInOut, int nVars, char * pCanonPerm )
{
    word pAux[1024], pAux1[1024];
    char tempArray[16];
    unsigned CanonPhase;
    assert( nVars <= 16 );
    CanonPhase = Kit_TruthSemiCanonicize_Yasha( pInOut, nVars, pCanonPerm );
    luckyCanonicizer(pInOut, pAux, pAux1, nVars, pCanonPerm, tempArray, &CanonPhase);
    return CanonPhase;
}

// this procedure is translates truth table from 'unsingeds' into 'words' 
unsigned Kit_TruthSemiCanonicize_new( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm )
{
    unsigned Result;
    if ( nVars < 6 )
    {
         word Temp = ((word)pInOut[0] << 32) | (word)pInOut[0];
         Result = Kit_TruthSemiCanonicize_new_internal( &Temp, nVars, pCanonPerm );
         pInOut[0] = (unsigned)Temp;
    }
    else
         Result = Kit_TruthSemiCanonicize_new_internal( (word *)pInOut, nVars, pCanonPerm );
    return Result;
}


// compile main() procedure only if running outside of ABC environment
#ifndef _RUNNING_ABC_

int main () 
{
//  char * pFileInput  = "nonDSDfunc06var1M.txt";
//  char * pFileInput1 = "partDSDfunc06var1M.txt";
//  char * pFileInput2 = "fullDSDfunc06var1M.txt";

//  char * pFileInput  = "nonDSDfunc10var100K.txt";
//  char * pFileInput1 = "partDSDfunc10var100K.txt";
//  char * pFileInput2 = "fullDSDfunc10var100K.txt";

//  char * pFileInput = "partDSDfunc12var100K.txt";
//  char * pFileInput  = "nonDSDfunc12var100K.txt";
//  char * pFileInput1 = "partDSDfunc12var100K.txt";
//  char * pFileInput2 = "fullDSDfunc12var100K.txt";

//  char * pFileInput  = "nonDSDfunc14var10K.txt";
//  char * pFileInput1 = "partDSDfunc14var10K.txt";
//  char * pFileInput2 = "fullDSDfunc14var10K.txt";

    char * pFileInput  = "nonDSDfunc16var10K.txt";
    char * pFileInput1 = "partDSDfunc16var10K.txt";
    char * pFileInput2 = "fullDSDfunc16var10K.txt";

    int i, j, tempNF;
    char** charArray;
    word** a, ** b;
    Abc_TtStore_t* p;
    word * pAux, * pAux1;
    int * pStore;
//  cycleCtr* cCtr;
    charArray = (char**)malloc(sizeof(char*)*3);

    charArray[0] = pFileInput;
    charArray[1] = pFileInput1;
    charArray[2] = pFileInput2;
    for(j=0;j<3;j++)
    {
        p = setTtStore(charArray[j]);   
//      p = setTtStore(pFileInput); 
        a = makeArray(p);
        b = makeArray(p);   
//      cCtr = setCycleCtrPtr();

        pAux = (word*)malloc(sizeof(word)*(p->nWords));
        pAux1 = (word*)malloc(sizeof(word)*(p->nWords));    
        pStore = (int*)malloc(sizeof(int)*(p->nVars));
        printf("In %s Fs at start = %d\n",charArray[j],p->nFuncs);
        
        tempNF = p->nFuncs;

        TimePrint("start");     
        for(i=0;i<p->nFuncs;i++)        
            luckyCanonicizer_final(a[i], pAux, pAux1, p->nVars, pStore);        
        TimePrint("done with A");

        sortAndUnique(a, p);
        printf("F left in A final = %d\n",p->nFuncs);
        freeArray(a,p);
        TimePrint("Done with sort");
        

// delete data-structures   
        free(pAux);
        free(pAux1);    
        free(pStore);
//      freeCycleCtr(cCtr);
        Abc_TruthStoreFree( p );
    }
    return 0;
}

#endif


ABC_NAMESPACE_IMPL_END