#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