#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