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

  FileName    [bm.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Boolean Matching package.]

  Synopsis    [Check P-equivalence and PP-equivalence of two circuits.]

  Author      [Hadi Katebi]
  
  Affiliation [University of Michigan]

  Date        [Ver. 1.0. Started - January, 2009.]

  Revision    [No revisions so far]

  Comments    [This is the cleaned up version of the code I used for DATE 2010 publication.]              
			  [If you have any question or if you find a bug, contact me at hadik@umich.edu.]
			  [I don't guarantee that I can fix all the bugs, but I can definitely point you to 
			   the right direction so you can fix the bugs yourself].

  Debugging   [There are some part of the code that are commented out. Those parts mostly print
               the contents of the data structures to the standard output. Un-comment them if you 
			   find them useful for debugging.]

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

#include "base/abc/abc.h"
#include "opt/sim/sim.h"
#include "sat/bsat/satSolver.h"
#include "misc/extra/extraBdd.h"

ABC_NAMESPACE_IMPL_START


int match1by1(Abc_Ntk_t * pNtk1, Vec_Ptr_t ** nodesInLevel1, Vec_Int_t ** iMatch1, Vec_Int_t ** iDep1, Vec_Int_t * matchedInputs1, int * iGroup1, Vec_Int_t ** oMatch1, int * oGroup1,
			   Abc_Ntk_t * pNtk2, Vec_Ptr_t ** nodesInLevel2, Vec_Int_t ** iMatch2, Vec_Int_t ** iDep2, Vec_Int_t * matchedInputs2, int * iGroup2, Vec_Int_t ** oMatch2, int * oGroup2,
			   Vec_Int_t * matchedOutputs1, Vec_Int_t * matchedOutputs2, Vec_Int_t * oMatchedGroups, Vec_Int_t * iNonSingleton, int ii, int idx);

int Abc_NtkBmSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Vec_Ptr_t * iMatchPairs, Vec_Ptr_t * oMatchPairs, Vec_Int_t * mismatch, int mode);

void getDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep)
{	
	Vec_Ptr_t * vSuppFun;
	int i, j;	
	
	vSuppFun = Sim_ComputeFunSupp(pNtk, 0);
	for(i = 0; i < Abc_NtkPoNum(pNtk); i++) {
		char * seg = (char *)vSuppFun->pArray[i];
		
		for(j = 0; j < Abc_NtkPiNum(pNtk); j+=8) {
			if(((*seg) & 0x01) == 0x01)
				Vec_IntPushOrder(oDep[i], j);
			if(((*seg) & 0x02) == 0x02)
				Vec_IntPushOrder(oDep[i], j+1);
			if(((*seg) & 0x04) == 0x04)
				Vec_IntPushOrder(oDep[i], j+2);
			if(((*seg) & 0x08) == 0x08)
				Vec_IntPushOrder(oDep[i], j+3);
			if(((*seg) & 0x10) == 0x10)
				Vec_IntPushOrder(oDep[i], j+4);
			if(((*seg) & 0x20) == 0x20)
				Vec_IntPushOrder(oDep[i], j+5);
			if(((*seg) & 0x40) == 0x40)
				Vec_IntPushOrder(oDep[i], j+6);
			if(((*seg) & 0x80) == 0x80)
				Vec_IntPushOrder(oDep[i], j+7);

			seg++;
		}
	}

	for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
		for(j = 0; j < Vec_IntSize(oDep[i]); j++)
			Vec_IntPush(iDep[Vec_IntEntry(oDep[i], j)], i);	
	

	/*for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
	{
		printf("Output %d: ", i);
		for(j = 0; j < Vec_IntSize(oDep[i]); j++)
			printf("%d ", Vec_IntEntry(oDep[i], j));
		printf("\n");
	}

	printf("\n");

	for(i = 0; i < Abc_NtkPiNum(pNtk); i++)
	{
		printf("Input %d: ", i);
		for(j = 0; j < Vec_IntSize(iDep[i]); j++)
			printf("%d ", Vec_IntEntry(iDep[i], j));
		printf("\n");
	}

	printf("\n");	*/	
}

void initMatchList(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep, Vec_Int_t** iMatch, int* iLastItem, Vec_Int_t** oMatch, int* oLastItem, int* iGroup, int* oGroup, int p_equivalence)
{
	int i, j, curr;
	Vec_Int_t** temp;

	if(!p_equivalence) {
		temp = ABC_ALLOC( Vec_Int_t*, Abc_NtkPiNum(pNtk)+1);

		for(i = 0; i < Abc_NtkPiNum(pNtk)+1; i++)	
			temp[i] = Vec_IntAlloc( 0 );	

		for(i = 0; i < Abc_NtkPoNum(pNtk); i++)		
			Vec_IntPush(temp[Vec_IntSize(oDep[i])], i);

		curr = 0;
		for(i = 0; i < Abc_NtkPiNum(pNtk)+1; i++)
		{
			if(Vec_IntSize(temp[i]) == 0)
				Vec_IntFree( temp[i] );

			else
			{
				oMatch[curr] = temp[i];
				
				for(j = 0; j < Vec_IntSize(temp[i]); j++)
					oGroup[Vec_IntEntry(oMatch[curr], j)] = curr;
			
				curr++;
			}
		}

		*oLastItem = curr;

		ABC_FREE( temp );
	}
	else {
		// the else part fixes the outputs for P-equivalence checking
		for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
		{
			Vec_IntPush(oMatch[i], i);
			oGroup[i] = i;
			(*oLastItem) = Abc_NtkPoNum(pNtk);
		}
	}
		
	/*for(j = 0; j < *oLastItem; j++)
	{
		printf("oMatch %d: ", j);
		for(i = 0; i < Vec_IntSize(oMatch[j]); i++)
			printf("%d ", Vec_IntEntry(oMatch[j], i));
		printf("\n");
	}

	for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
		printf("%d: %d ", i, oGroup[i]);*/

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

	temp = ABC_ALLOC( Vec_Int_t*, Abc_NtkPoNum(pNtk)+1 );

	for(i = 0; i < Abc_NtkPoNum(pNtk)+1; i++)	
		temp[i] = Vec_IntAlloc( 0 );

	for(i = 0; i < Abc_NtkPiNum(pNtk); i++)		
		Vec_IntPush(temp[Vec_IntSize(iDep[i])], i);

	curr = 0;
	for(i = 0; i < Abc_NtkPoNum(pNtk)+1; i++)
	{
		if(Vec_IntSize(temp[i]) == 0)
			Vec_IntFree( temp[i] );
		else
		{
			iMatch[curr] = temp[i];
			for(j = 0; j < Vec_IntSize(iMatch[curr]); j++)
				iGroup[Vec_IntEntry(iMatch[curr], j)] = curr;
			curr++;
		}		
	}

	*iLastItem = curr;

	ABC_FREE( temp );		

	/*printf("\n");
	for(j = 0; j < *iLastItem; j++)
	{
		printf("iMatch %d: ", j);
		for(i = 0; i < Vec_IntSize(iMatch[j]); i++)
			printf("%d ", Vec_IntEntry(iMatch[j], i));
		printf("\n");
	}

	for(i = 0; i < Abc_NtkPiNum(pNtk); i++)
		printf("%d: %d ", i, iGroup[i]);
	printf("\n");*/
}

void iSortDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, int* oGroup)
{
	int i, j, k;	
	Vec_Int_t * temp;	
	Vec_Int_t * oGroupList;	

	oGroupList = Vec_IntAlloc( 10 );

	for(i = 0; i < Abc_NtkPiNum(pNtk); i++)
	{
		if(Vec_IntSize(iDep[i]) == 1)
			continue;
		
		temp = Vec_IntAlloc( Vec_IntSize(iDep[i]) );		

		for(j = 0; j < Vec_IntSize(iDep[i]); j++)
			Vec_IntPushUniqueOrder(oGroupList, oGroup[Vec_IntEntry(iDep[i], j)]);

		for(j = 0; j < Vec_IntSize(oGroupList); j++)
		{
			for(k = 0; k < Vec_IntSize(iDep[i]); k++)
				if(oGroup[Vec_IntEntry(iDep[i], k)] == Vec_IntEntry(oGroupList, j))
				{
					Vec_IntPush( temp, Vec_IntEntry(iDep[i], k) );		
					Vec_IntRemove( iDep[i], Vec_IntEntry(iDep[i], k) );
					k--;
				}
		}		

		Vec_IntFree( iDep[i] );		
		iDep[i] = temp;
		Vec_IntClear( oGroupList );

		/*printf("Input %d: ", i);
		for(j = 0; j < Vec_IntSize(iDep[i]); j++)
			printf("%d ", Vec_IntEntry(iDep[i], j));
		printf("\n");*/
	}
	
	Vec_IntFree( oGroupList );
}

void oSortDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** oDep, int* iGroup)
{
	int i, j, k;	
	Vec_Int_t * temp;
	Vec_Int_t * iGroupList;	
	
	iGroupList = Vec_IntAlloc( 10 );

	for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
	{
		if(Vec_IntSize(oDep[i]) == 1)
			continue;	
		
		temp = Vec_IntAlloc( Vec_IntSize(oDep[i]) );

		for(j = 0; j < Vec_IntSize(oDep[i]); j++)
			Vec_IntPushUniqueOrder(iGroupList, iGroup[Vec_IntEntry(oDep[i], j)]);		

		for(j = 0; j < Vec_IntSize(iGroupList); j++)
		{
			for(k = 0; k < Vec_IntSize(oDep[i]); k++)
				if(iGroup[Vec_IntEntry(oDep[i], k)] == Vec_IntEntry(iGroupList, j))
				{
					Vec_IntPush( temp, Vec_IntEntry(oDep[i], k) );
					Vec_IntRemove( oDep[i], Vec_IntEntry(oDep[i], k) );
					k--;
				}
		}

		Vec_IntFree( oDep[i] );
		oDep[i] = temp;
		Vec_IntClear( iGroupList );

		/*printf("Output %d: ", i);
		for(j = 0; j < Vec_IntSize(oDep[i]); j++)
			printf("%d ", Vec_IntEntry(oDep[i], j));
		printf("\n");*/
	}
	
	Vec_IntFree( iGroupList );
}

int oSplitByDep(Abc_Ntk_t *pNtk, Vec_Int_t** oDep, Vec_Int_t** oMatch, int* oGroup, int* oLastItem, int* iGroup)
{
	int i, j, k;
	int numOfItemsAdded;
	Vec_Int_t * array, * sortedArray;	

	numOfItemsAdded = 0;

	for(i = 0; i < *oLastItem; i++)
	{
		if(Vec_IntSize(oMatch[i]) == 1)
			continue;

		array = Vec_IntAlloc( Vec_IntSize(oMatch[i]) );
		sortedArray = Vec_IntAlloc( Vec_IntSize(oMatch[i]) );

		for(j = 0; j < Vec_IntSize(oMatch[i]); j++)
		{
			int factor, encode;

			encode = 0;
			factor = 1;	
			
			for(k = 0; k < Vec_IntSize(oDep[Vec_IntEntry(oMatch[i], j)]); k++)										
				encode += iGroup[Vec_IntEntry(oDep[Vec_IntEntry(oMatch[i], j)], k)] * factor;						
			
			Vec_IntPush(array, encode);
			Vec_IntPushUniqueOrder(sortedArray, encode);

			if( encode < 0)
				printf("WARNING! Integer overflow!");

			//printf("%d ", Vec_IntEntry(array, j));
		}				
		
		while( Vec_IntSize(sortedArray) > 1 )
		{			
			for(k = 0; k < Vec_IntSize(oMatch[i]); k++) 
			{
				if(Vec_IntEntry(array, k) == Vec_IntEntryLast(sortedArray))
				{
					Vec_IntPush(oMatch[*oLastItem+numOfItemsAdded], Vec_IntEntry(oMatch[i], k));
					oGroup[Vec_IntEntry(oMatch[i], k)] = *oLastItem+numOfItemsAdded;
					Vec_IntRemove( oMatch[i], Vec_IntEntry(oMatch[i], k) );		
					Vec_IntRemove( array, Vec_IntEntry(array, k) );			
					k--;
				}	
			}			
			numOfItemsAdded++;
			Vec_IntPop(sortedArray);						
		}

		Vec_IntFree( array );		
		Vec_IntFree( sortedArray );		
		//printf("\n");
	}	

	*oLastItem += numOfItemsAdded;

	/*printf("\n");
	for(j = 0; j < *oLastItem ; j++)
	{
		printf("oMatch %d: ", j);
		for(i = 0; i < Vec_IntSize(oMatch[j]); i++)
			printf("%d ", Vec_IntEntry(oMatch[j], i));
		printf("\n");
	}*/

	return numOfItemsAdded;
}

int iSplitByDep(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** iMatch, int* iGroup, int* iLastItem, int* oGroup)
{
	int i, j, k;	
	int numOfItemsAdded = 0;
	Vec_Int_t * array, * sortedArray;	

	for(i = 0; i < *iLastItem; i++)
	{
		if(Vec_IntSize(iMatch[i]) == 1)
			continue;
		
		array = Vec_IntAlloc( Vec_IntSize(iMatch[i]) );
		sortedArray = Vec_IntAlloc( Vec_IntSize(iMatch[i]) );

		for(j = 0; j < Vec_IntSize(iMatch[i]); j++)
		{		
			int factor, encode;

			encode = 0;
			factor = 1;	
			
			for(k = 0; k < Vec_IntSize(iDep[Vec_IntEntry(iMatch[i], j)]); k++)							
				encode += oGroup[Vec_IntEntry(iDep[Vec_IntEntry(iMatch[i], j)], k)] * factor;						

			Vec_IntPush(array, encode);
			Vec_IntPushUniqueOrder(sortedArray, encode);
			
			//printf("%d ", Vec_IntEntry(array, j));
		}			
				
		while( Vec_IntSize(sortedArray) > 1 )
		{			
			for(k = 0; k < Vec_IntSize(iMatch[i]); k++) 
			{
				if(Vec_IntEntry(array, k) == Vec_IntEntryLast(sortedArray))
				{
					Vec_IntPush(iMatch[*iLastItem+numOfItemsAdded], Vec_IntEntry(iMatch[i], k));
					iGroup[Vec_IntEntry(iMatch[i], k)] = *iLastItem+numOfItemsAdded;
					Vec_IntRemove( iMatch[i], Vec_IntEntry(iMatch[i], k) );							
					Vec_IntRemove( array, Vec_IntEntry(array, k) );	
					k--;
				}
			}
			numOfItemsAdded++;
			Vec_IntPop(sortedArray);	
		}

		Vec_IntFree( array );		
		Vec_IntFree( sortedArray );	
		//printf("\n");
	}	

	*iLastItem += numOfItemsAdded;

	/*printf("\n");
	for(j = 0; j < *iLastItem ; j++)
	{
		printf("iMatch %d: ", j);
		for(i = 0; i < Vec_IntSize(iMatch[j]); i++)
			printf("%d ", Vec_IntEntry(iMatch[j], i));
		printf("\n");
	}*/

	return numOfItemsAdded;	
}

Vec_Ptr_t ** findTopologicalOrder( Abc_Ntk_t * pNtk )
{
    Vec_Ptr_t ** vNodes;
    Abc_Obj_t * pObj, * pFanout;
    int i, k;    
    
	extern void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
	
	// start the array of nodes
    vNodes = ABC_ALLOC(Vec_Ptr_t *, Abc_NtkPiNum(pNtk));
	for(i = 0; i < Abc_NtkPiNum(pNtk); i++)
		vNodes[i] = Vec_PtrAlloc(50);	
	
    Abc_NtkForEachCi( pNtk, pObj, i )
    {
		// set the traversal ID
		Abc_NtkIncrementTravId( pNtk );
        Abc_NodeSetTravIdCurrent( pObj );
        pObj = Abc_ObjFanout0Ntk(pObj);
        Abc_ObjForEachFanout( pObj, pFanout, k )
            Abc_NtkDfsReverse_rec( pFanout, vNodes[i] );
    }
   
    return vNodes;
}


int * Abc_NtkSimulateOneNode( Abc_Ntk_t * pNtk, int * pModel, int input, Vec_Ptr_t ** topOrder )
{
    Abc_Obj_t * pNode;
	Vec_Ptr_t * vNodes;
    int * pValues, Value0, Value1, i;
   
	vNodes = Vec_PtrAlloc( 50 );
/*
    printf( "Counter example: " );
    Abc_NtkForEachCi( pNtk, pNode, i )
        printf( " %d", pModel[i] );
    printf( "\n" );
*/
    // increment the trav ID
    Abc_NtkIncrementTravId( pNtk );
    // set the CI values     
	Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)1;
	pNode = Abc_NtkCi(pNtk, input);
	pNode->iTemp = pModel[input];
	
    // simulate in the topological order	
    for(i = Vec_PtrSize(topOrder[input])-1; i >= 0; i--)
    {
		pNode = (Abc_Obj_t *)Vec_PtrEntry(topOrder[input], i);		
		
        Value0 = ((int)(ABC_PTRUINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
        Value1 = ((int)(ABC_PTRUINT_T)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode);
        
		if( pNode->iTemp != (Value0 & Value1))
		{
			pNode->iTemp = (Value0 & Value1);
			Vec_PtrPush(vNodes, pNode);
		}
	
    }	
    // fill the output values
    pValues = ABC_ALLOC( int, Abc_NtkCoNum(pNtk) );
    Abc_NtkForEachCo( pNtk, pNode, i )
        pValues[i] = ((int)(ABC_PTRUINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
    
	pNode = Abc_NtkCi(pNtk, input);
	if(pNode->pCopy == (Abc_Obj_t *)1)
		pNode->pCopy = (Abc_Obj_t *)0;
	else
		pNode->pCopy = (Abc_Obj_t *)1;

	for(i = 0; i < Vec_PtrSize(vNodes); i++)
	{
		pNode = (Abc_Obj_t *)Vec_PtrEntry(vNodes, i);

		if(pNode->pCopy == (Abc_Obj_t *)1)
			pNode->pCopy = (Abc_Obj_t *)0;
		else
			pNode->pCopy = (Abc_Obj_t *)1;
	}

	Vec_PtrFree( vNodes );

    return pValues;
}

int refineIOBySimulation(Abc_Ntk_t *pNtk, Vec_Int_t** iMatch, int* iLastItem, int * iGroup, Vec_Int_t** iDep, Vec_Int_t** oMatch, int* oLastItem, int * oGroup, Vec_Int_t** oDep, char * vPiValues, int * observability, Vec_Ptr_t ** topOrder)
{
	Abc_Obj_t * pObj;
	int * pModel;//, ** pModel2;
	int * output, * output2;
	int lastItem;
	int i, j, k;
	Vec_Int_t * iComputedNum, * iComputedNumSorted;	
	Vec_Int_t * oComputedNum;				// encoding the number of flips		
	int factor;	
	int isRefined = FALSE;	

	pModel = ABC_ALLOC( int, Abc_NtkCiNum(pNtk) );	

	Abc_NtkForEachPi( pNtk, pObj, i )
		pModel[i] = vPiValues[i] - '0';
	Abc_NtkForEachLatch( pNtk, pObj, i )
		pModel[Abc_NtkPiNum(pNtk)+i] = pObj->iData - 1;

	output = Abc_NtkVerifySimulatePattern( pNtk, pModel );	

	oComputedNum = Vec_IntAlloc( Abc_NtkPoNum(pNtk) );
	for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
		Vec_IntPush(oComputedNum, 0);
	
	/****************************************************************************************/
	/********** group outputs that produce 1 and outputs that produce 0 together ************/	
	
	lastItem = *oLastItem;
	for(i = 0; i < lastItem && (*oLastItem) != Abc_NtkPoNum(pNtk); i++)
	{
		int flag = FALSE;

		if(Vec_IntSize(oMatch[i]) == 1)
			continue;

		for(j = 1; j < Vec_IntSize(oMatch[i]); j++)
			if(output[Vec_IntEntry(oMatch[i], 0)] != output[Vec_IntEntry(oMatch[i], j)])
			{
				flag = TRUE;
				break;
			}

		if(flag)
		{
			for(j = 0; j < Vec_IntSize(oMatch[i]); j++)
				if(output[Vec_IntEntry(oMatch[i], j)])
				{
					Vec_IntPush(oMatch[*oLastItem], Vec_IntEntry(oMatch[i], j));
					oGroup[Vec_IntEntry(oMatch[i], j)] = *oLastItem;	
					Vec_IntRemove(oMatch[i], Vec_IntEntry(oMatch[i], j));	
					j--;
				}

			(*oLastItem)++;
		}
	}

	if( (*oLastItem) > lastItem )
	{
		isRefined = TRUE;
		iSortDependencies(pNtk, iDep, oGroup);	
	}

	/****************************************************************************************/
	/************* group inputs that make the same number of flips in outpus ****************/		

	lastItem = *iLastItem;
	for(i = 0; i < lastItem && (*iLastItem) != Abc_NtkPiNum(pNtk); i++)
	{
		int num;

		if(Vec_IntSize(iMatch[i]) == 1)
			continue;

		iComputedNum = Vec_IntAlloc( Vec_IntSize(iMatch[i]) );
		iComputedNumSorted = Vec_IntAlloc( Vec_IntSize(iMatch[i]) );	
		
		for(j = 0; j < Vec_IntSize(iMatch[i]); j++)
		{
			if( vPiValues[Vec_IntEntry(iMatch[i], j)] == '0' )				
				pModel[Vec_IntEntry(iMatch[i], j)] = 1;
			else 				
				pModel[Vec_IntEntry(iMatch[i], j)] = 0;		
			
			//output2 = Abc_NtkVerifySimulatePattern( pNtk, pModel );	
			output2 = Abc_NtkSimulateOneNode( pNtk, pModel, Vec_IntEntry(iMatch[i], j), topOrder );
			
			num = 0;
			factor = 1;	
			for(k = 0; k < Vec_IntSize(iDep[Vec_IntEntry(iMatch[i], j)]); k++)
			{
				int outputIndex = Vec_IntEntry(iDep[Vec_IntEntry(iMatch[i], j)], k);		

				if(output2[outputIndex])
					num += (oGroup[outputIndex] + 1) * factor;				
			
				if(output[outputIndex] != output2[outputIndex])
				{
					int temp = Vec_IntEntry(oComputedNum, outputIndex) + i + 1;
					Vec_IntWriteEntry(oComputedNum, outputIndex, temp);	
					observability[Vec_IntEntry(iMatch[i], j)]++;
				}
			}

			Vec_IntPush(iComputedNum, num);
			Vec_IntPushUniqueOrder(iComputedNumSorted, num);			

			pModel[Vec_IntEntry(iMatch[i], j)] = vPiValues[Vec_IntEntry(iMatch[i], j)] - '0';
			ABC_FREE( output2 );
		}	

		while( Vec_IntSize( iComputedNumSorted ) > 1 )
		{
			for(k = 0; k < Vec_IntSize(iMatch[i]); k++)
			{							
				if(Vec_IntEntry(iComputedNum, k) == Vec_IntEntryLast(iComputedNumSorted) )
				{
					Vec_IntPush(iMatch[*iLastItem], Vec_IntEntry(iMatch[i], k));
					iGroup[Vec_IntEntry(iMatch[i], k)] = *iLastItem;
					Vec_IntRemove( iMatch[i], Vec_IntEntry(iMatch[i], k) );
					Vec_IntRemove( iComputedNum, Vec_IntEntry(iComputedNum, k) );		
					k--;
				}				
			}
			(*iLastItem)++;	
			Vec_IntPop( iComputedNumSorted );
		}	

		Vec_IntFree( iComputedNum );
		Vec_IntFree( iComputedNumSorted );
	}

	if( (*iLastItem) > lastItem )
	{
		isRefined = TRUE;
		oSortDependencies(pNtk, oDep, iGroup);
	}

	/****************************************************************************************/
	/********** encode the number of flips in each output by flipping the outputs ***********/
	/********** and group all the outputs that have the same encoding         ***********/	

	lastItem = *oLastItem;
	for(i = 0; i < lastItem && (*oLastItem) != Abc_NtkPoNum(pNtk); i++)
	{
		Vec_Int_t * encode, * sortedEncode;				// encoding the number of flips					

		if(Vec_IntSize(oMatch[i]) == 1)
			continue;
			
		encode = Vec_IntAlloc( Vec_IntSize(oMatch[i]) );
		sortedEncode = Vec_IntAlloc( Vec_IntSize(oMatch[i]) );					
	
		for(j = 0; j < Vec_IntSize(oMatch[i]); j++)
		{
			Vec_IntPush(encode, Vec_IntEntry(oComputedNum, Vec_IntEntry(oMatch[i], j)) );
			Vec_IntPushUniqueOrder( sortedEncode, Vec_IntEntry(encode, j) );
		}

		while( Vec_IntSize(sortedEncode) > 1 )
		{
			for(j = 0; j < Vec_IntSize(oMatch[i]); j++)
				if(Vec_IntEntry(encode, j) == Vec_IntEntryLast(sortedEncode))
				{
					Vec_IntPush(oMatch[*oLastItem], Vec_IntEntry(oMatch[i], j));
					oGroup[Vec_IntEntry(oMatch[i], j)] = *oLastItem;
					Vec_IntRemove( oMatch[i], Vec_IntEntry(oMatch[i], j) );
					Vec_IntRemove( encode, Vec_IntEntry(encode, j) );
					j --;
				}				
			
			(*oLastItem)++;
			Vec_IntPop( sortedEncode );
		}

		Vec_IntFree( encode );
		Vec_IntFree( sortedEncode );
	}

	if( (*oLastItem) > lastItem )
		isRefined = TRUE;	

	ABC_FREE( pModel );
	ABC_FREE( output );
	Vec_IntFree( oComputedNum );

	return isRefined;	
}

Abc_Ntk_t * Abc_NtkMiterBm( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Vec_Ptr_t * iCurrMatch, Vec_Ptr_t * oCurrMatch )
{
	char Buffer[1000];
    Abc_Ntk_t * pNtkMiter;

	pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
    sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
    pNtkMiter->pName = Extra_UtilStrsav(Buffer);

	//Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );
	{
		Abc_Obj_t * pObj, * pObjNew;
		int i;

		Abc_AigConst1(pNtk1)->pCopy = Abc_AigConst1(pNtkMiter);
		Abc_AigConst1(pNtk2)->pCopy = Abc_AigConst1(pNtkMiter);

		// create new PIs and remember them in the old PIs
		if(iCurrMatch == NULL)
		{
			Abc_NtkForEachCi( pNtk1, pObj, i )
			{
				pObjNew = Abc_NtkCreatePi( pNtkMiter );
				// remember this PI in the old PIs
				pObj->pCopy = pObjNew;
				pObj = Abc_NtkCi(pNtk2, i);  
				pObj->pCopy = pObjNew;
				// add name
				Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL );
			}
		}
		else
		{
			for(i = 0; i < Vec_PtrSize( iCurrMatch ); i += 2)
			{
				pObjNew = Abc_NtkCreatePi( pNtkMiter );
				pObj = (Abc_Obj_t *)Vec_PtrEntry(iCurrMatch, i);
				pObj->pCopy = pObjNew;
				pObj = (Abc_Obj_t *)Vec_PtrEntry(iCurrMatch, i+1);
				pObj->pCopy = pObjNew;
				// add name
				Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL );
			}
		}

        // create the only PO
        pObjNew = Abc_NtkCreatePo( pNtkMiter );
        // add the PO name
        Abc_ObjAssignName( pObjNew, "miter", NULL );
	}

	// Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
	{
		Abc_Obj_t * pNode;
		int i;
		assert( Abc_NtkIsDfsOrdered(pNtk1) );
		Abc_AigForEachAnd( pNtk1, pNode, i )
			pNode->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkMiter->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
	}

	// Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
	{
		Abc_Obj_t * pNode;
		int i;
		assert( Abc_NtkIsDfsOrdered(pNtk2) );
		Abc_AigForEachAnd( pNtk2, pNode, i )
			pNode->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkMiter->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
	}
	
	// Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );	
	{
		Vec_Ptr_t * vPairs;
		Abc_Obj_t * pMiter;
		int i;

		vPairs = Vec_PtrAlloc( 100 );
	    
		// collect the CO nodes for the miter
		if(oCurrMatch != NULL)
		{
			for(i = 0; i < Vec_PtrSize( oCurrMatch ); i += 2)
			{
				Vec_PtrPush( vPairs, Abc_ObjChild0Copy((Abc_Obj_t *)Vec_PtrEntry(oCurrMatch, i)) );
				Vec_PtrPush( vPairs, Abc_ObjChild0Copy((Abc_Obj_t *)Vec_PtrEntry(oCurrMatch, i+1)) );
			}
		}
		else
		{
			Abc_Obj_t * pNode;

			Abc_NtkForEachCo( pNtk1, pNode, i )
			{
				Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
				pNode = Abc_NtkCo( pNtk2, i );
				Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
			}
		}
		
	 pMiter = Abc_AigMiter( (Abc_Aig_t *)pNtkMiter->pManFunc, vPairs, 0 );
	 Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
	 Vec_PtrFree(vPairs);
	}

	//Abc_AigCleanup(pNtkMiter->pManFunc);
	
	return pNtkMiter;
}

int * pValues1__, * pValues2__;

void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, Vec_Int_t * mismatch )
{
    Vec_Ptr_t * vNodes;
    Abc_Obj_t * pNode;    
    int nErrors, nPrinted, i, iNode = -1;

    assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
    assert( Abc_NtkCoNum(pNtk1) == Abc_NtkCoNum(pNtk2) );
    // get the CO values under this model
    pValues1__ = Abc_NtkVerifySimulatePattern( pNtk1, pModel );
    pValues2__ = Abc_NtkVerifySimulatePattern( pNtk2, pModel );
    // count the mismatches
    nErrors = 0;
    for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
        nErrors += (int)( pValues1__[i] != pValues2__[i] );
    //printf( "Verification failed for at least %d outputs: ", nErrors );
    // print the first 3 outputs
    nPrinted = 0;
    for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
        if ( pValues1__[i] != pValues2__[i] )
        {
            if ( iNode == -1 )
                iNode = i;
            //printf( " %s", Abc_ObjName(Abc_NtkCo(pNtk1,i)) );
            if ( ++nPrinted == 3 )
                break;
        }
    /*if ( nPrinted != nErrors )
        printf( " ..." );
    printf( "\n" );*/
    // report mismatch for the first output
    if ( iNode >= 0 )
    {
        /*printf( "Output %s: Value in Network1 = %d. Value in Network2 = %d.\n", 
            Abc_ObjName(Abc_NtkCo(pNtk1,iNode)), pValues1[iNode], pValues2[iNode] );
        printf( "Input pattern: " );*/
        // collect PIs in the cone
        pNode = Abc_NtkCo(pNtk1,iNode);
        vNodes = Abc_NtkNodeSupport( pNtk1, &pNode, 1 );
        // set the PI numbers
        Abc_NtkForEachCi( pNtk1, pNode, i )
            pNode->iTemp = i;
        // print the model
        pNode = (Abc_Obj_t *)Vec_PtrEntry( vNodes, 0 );
        if ( Abc_ObjIsCi(pNode) )
        {
            Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
            {
                assert( Abc_ObjIsCi(pNode) );
                //printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)pNode->pCopy] );
				Vec_IntPush(mismatch, Abc_ObjId(pNode)-1);
				Vec_IntPush(mismatch, pModel[(int)(size_t)pNode->pCopy]);
            }
        }
        //printf( "\n" );
        Vec_PtrFree( vNodes );
    }
    free( pValues1__ );
    free( pValues2__ );
}

int Abc_NtkMiterSatBm( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fVerbose, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects)
{
    static sat_solver * pSat = NULL;
    lbool   status;
    int RetValue;
    abctime clk;	

	extern int Abc_NodeAddClausesTop( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
	extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );	
 
    if ( pNumConfs )
        *pNumConfs = 0;
    if ( pNumInspects )
        *pNumInspects = 0;

    assert( Abc_NtkLatchNum(pNtk) == 0 );

//    if ( Abc_NtkPoNum(pNtk) > 1 )
//        fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );

    // load clauses into the sat_solver
    clk = Abc_Clock();

			
		
	pSat = (sat_solver *)Abc_NtkMiterSatCreate( pNtk, 0 );
			
    if ( pSat == NULL )
        return 1;
//printf( "%d \n", pSat->clauses.size );
//sat_solver_delete( pSat );
//return 1;

//    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
//    PRT( "Time", Abc_Clock() - clk );

    // simplify the problem
    clk = Abc_Clock();
    status = sat_solver_simplify(pSat);
//    printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
//    PRT( "Time", Abc_Clock() - clk );
    if ( status == 0 )
    {
        sat_solver_delete( pSat );
//        printf( "The problem is UNSATISFIABLE after simplification.\n" );
        return 1;
    }

    // solve the miter
    clk = Abc_Clock();
    if ( fVerbose )
        pSat->verbosity = 1;
    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    if ( status == l_Undef )
    {
//        printf( "The problem timed out.\n" );
        RetValue = -1;
    }
    else if ( status == l_True )
    {
//        printf( "The problem is SATISFIABLE.\n" );
        RetValue = 0;
    }
    else if ( status == l_False )
    {
//        printf( "The problem is UNSATISFIABLE.\n" );
        RetValue = 1;
    }
    else
        assert( 0 );
//    PRT( "SAT sat_solver time", Abc_Clock() - clk );
//    printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );

    // if the problem is SAT, get the counterexample
    if ( status == l_True )
    {
//        Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
        Vec_Int_t * vCiIds = Abc_NtkGetCiSatVarNums( pNtk );
        pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
        Vec_IntFree( vCiIds );
    }
    // free the sat_solver
    if ( fVerbose )
        Sat_SolverPrintStats( stdout, pSat );

    if ( pNumConfs )
        *pNumConfs = (int)pSat->stats.conflicts;
    if ( pNumInspects )
        *pNumInspects = (int)pSat->stats.inspects;

//sat_solver_store_write( pSat, "trace.cnf" );	
	sat_solver_store_free( pSat );
	sat_solver_delete( pSat );
    return RetValue;
}

int Abc_NtkBmSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Vec_Ptr_t * iMatchPairs, Vec_Ptr_t * oMatchPairs, Vec_Int_t * mismatch, int mode)
{    
    extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );	

	Abc_Ntk_t * pMiter = NULL;
    Abc_Ntk_t * pCnf;
    int RetValue;

	// get the miter of the two networks
	if( mode == 0 )
	{
		//Abc_NtkDelete( pMiter );
		pMiter = Abc_NtkMiterBm( pNtk1, pNtk2, iMatchPairs, oMatchPairs );
	}
	else if( mode == 1 )		// add new outputs
	{		
		int i;
		Abc_Obj_t * pObj;
		Vec_Ptr_t * vPairs;
		Abc_Obj_t * pNtkMiter;		

		vPairs = Vec_PtrAlloc( 100 );

		Abc_NtkForEachCo( pMiter, pObj, i )			
			Abc_ObjRemoveFanins( pObj );

		for(i = 0; i < Vec_PtrSize( oMatchPairs ); i += 2)
		{
			Vec_PtrPush( vPairs, Abc_ObjChild0Copy((Abc_Obj_t *)Vec_PtrEntry(oMatchPairs, i)) );
			Vec_PtrPush( vPairs, Abc_ObjChild0Copy((Abc_Obj_t *)Vec_PtrEntry(oMatchPairs, i+1)) );
		}
		pNtkMiter = Abc_AigMiter( (Abc_Aig_t *)pMiter->pManFunc, vPairs, 0 );
		Abc_ObjAddFanin( Abc_NtkPo(pMiter,0), pNtkMiter );	 
		Vec_PtrFree( vPairs);
	}
	else if( mode == 2 )		// add some outputs
	{

	}
	else if( mode == 3)			// remove all outputs
	{
	}

	if ( pMiter == NULL )
	{
		printf("Miter computation has failed.");		
		return -1;
	}
	RetValue = Abc_NtkMiterIsConstant( pMiter );
	if ( RetValue == 0)
	{		
		/*printf("Networks are NOT EQUIVALENT after structural hashing.");	*/
		// report the error    	
		if(mismatch != NULL)
		{
			pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
			Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel, mismatch );
			ABC_FREE( pMiter->pModel );
		}        
		Abc_NtkDelete( pMiter );
        return RetValue;
	}
	if( RetValue == 1 )
	{		
		/*printf("Networks are equivalent after structural hashing.");	*/
		Abc_NtkDelete( pMiter );
		return RetValue;
	}

	// convert the miter into a CNF
	//if(mode == 0)
	pCnf = Abc_NtkMulti( pMiter, 0, 100, 1, 0, 0, 0 );
    Abc_NtkDelete( pMiter );
    if ( pCnf == NULL )
    {        
		printf("Renoding for CNF has failed.");	
        return -1;
    }

    // solve the CNF using the SAT solver
    RetValue = Abc_NtkMiterSat( pCnf, (ABC_INT64_T)10000, (ABC_INT64_T)0, 0, NULL, NULL);
    /*if ( RetValue == -1 )
		printf("Networks are undecided (SAT solver timed out).");	
    else if ( RetValue == 0 )        
		printf("Networks are NOT EQUIVALENT after SAT.");	
    else
		printf("Networks are equivalent after SAT.");	*/
	if ( mismatch != NULL && pCnf->pModel )
        Abc_NtkVerifyReportError( pNtk1, pNtk2, pCnf->pModel, mismatch );

    ABC_FREE( pCnf->pModel );
    Abc_NtkDelete( pCnf );

	return RetValue;
}

int checkEquivalence( Abc_Ntk_t * pNtk1, Vec_Int_t* matchedInputs1, Vec_Int_t * matchedOutputs1,
					   Abc_Ntk_t * pNtk2, Vec_Int_t* matchedInputs2, Vec_Int_t * matchedOutputs2)
{	
	Vec_Ptr_t * iMatchPairs, * oMatchPairs;
	int i;
	int result;

	iMatchPairs = Vec_PtrAlloc( Abc_NtkPiNum( pNtk1 ) * 2);
	oMatchPairs = Vec_PtrAlloc( Abc_NtkPoNum( pNtk1 ) * 2);

	for(i = 0; i < Abc_NtkPiNum(pNtk1); i++)
	{	
		Vec_PtrPush(iMatchPairs, Abc_NtkPi(pNtk2, Vec_IntEntry(matchedInputs2, i)));
		Vec_PtrPush(iMatchPairs, Abc_NtkPi(pNtk1, Vec_IntEntry(matchedInputs1, i)));
	}
				

	for(i = 0; i < Abc_NtkPoNum(pNtk1); i++)		
	{
		Vec_PtrPush(oMatchPairs, Abc_NtkPo(pNtk2, Vec_IntEntry(matchedOutputs2, i)));
		Vec_PtrPush(oMatchPairs, Abc_NtkPo(pNtk1, Vec_IntEntry(matchedOutputs1, i)));
	}		

	result = Abc_NtkBmSat(pNtk1, pNtk2, iMatchPairs, oMatchPairs, NULL, 0);

	if( result )
		printf("*** Circuits are equivalent ***\n");
	else
		printf("*** Circuits are NOT equivalent ***\n");

	Vec_PtrFree( iMatchPairs );
	Vec_PtrFree( oMatchPairs );	

	return result;
}

Abc_Ntk_t * computeCofactor(Abc_Ntk_t * pNtk, Vec_Ptr_t ** nodesInLevel, int * bitVector, Vec_Int_t * currInputs)
{	
	Abc_Ntk_t * subNtk;	
	Abc_Obj_t * pObj, * pObjNew;
	int i, j, numOfLevels;		

	numOfLevels = Abc_AigLevel( pNtk );		// number of levels excludes PI/POs	

	// start a new network
	subNtk = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );    
    subNtk->pName = Extra_UtilStrsav("subNtk");

	Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(subNtk);	

	// clean the node copy fields and mark the nodes that need to be copied to the new network
    Abc_NtkCleanCopy( pNtk );

	if(bitVector != NULL)
	{
		for(i = 0; i < Abc_NtkPiNum(pNtk); i++)
			if(bitVector[i])
			{
				pObj = Abc_NtkPi(pNtk, i);
				pObj->pCopy = (Abc_Obj_t *)(1);
			}
	}

	for(i = 0; i < Vec_IntSize(currInputs); i++)
	{
		pObj = Abc_NtkPi(pNtk, Vec_IntEntry(currInputs, i));
		pObjNew = Abc_NtkDupObj( subNtk, pObj, 1 );
		pObj->pCopy = pObjNew;
	}
		

	// i = 0 are the inputs and the inputs are not added to the 2d array ( nodesInLevel )
	for( i = 0; i <= numOfLevels; i++ )	
		for( j = 0; j < Vec_PtrSize( nodesInLevel[i] ); j++)
		{
			pObj = (Abc_Obj_t *)Vec_PtrEntry( nodesInLevel[i], j );

			if(Abc_ObjChild0Copy(pObj) == NULL && Abc_ObjChild1Copy(pObj) == NULL)
				pObj->pCopy = NULL;
			else if(Abc_ObjChild0Copy(pObj) == NULL && Abc_ObjChild1Copy(pObj) == (void*)(1))
				pObj->pCopy = NULL;
			else if(Abc_ObjChild0Copy(pObj) == NULL && (Abc_ObjChild1Copy(pObj) != (NULL) && Abc_ObjChild1Copy(pObj) != (void*)(1)) )
				pObj->pCopy = NULL;
			else if(Abc_ObjChild0Copy(pObj) == (void*)(1) && Abc_ObjChild1Copy(pObj) == NULL)
				pObj->pCopy = NULL;
			else if(Abc_ObjChild0Copy(pObj) == (void*)(1) && Abc_ObjChild1Copy(pObj) == (void*)(1))
				pObj->pCopy = (Abc_Obj_t *)(1);
			else if(Abc_ObjChild0Copy(pObj) == (void*)(1) && (Abc_ObjChild1Copy(pObj) != (NULL) && Abc_ObjChild1Copy(pObj) != (void*)(1)) )
				pObj->pCopy = Abc_ObjChild1Copy(pObj);
			else if( (Abc_ObjChild0Copy(pObj) != (NULL) && Abc_ObjChild0Copy(pObj) != (void*)(1)) && Abc_ObjChild1Copy(pObj) == NULL )
				pObj->pCopy = NULL;
			else if( (Abc_ObjChild0Copy(pObj) != (NULL) && Abc_ObjChild0Copy(pObj) != (void*)(1)) && Abc_ObjChild1Copy(pObj) == (void*)(1) )
				pObj->pCopy = Abc_ObjChild0Copy(pObj);
			else if( (Abc_ObjChild0Copy(pObj) != (NULL) && Abc_ObjChild0Copy(pObj) != (void*)(1)) &&
					 (Abc_ObjChild1Copy(pObj) != (NULL) && Abc_ObjChild1Copy(pObj) != (void*)(1)) )
				pObj->pCopy = Abc_AigAnd( (Abc_Aig_t *)subNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );					
		}	

	for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
	{
		pObj = Abc_NtkPo(pNtk, i);
		pObjNew = Abc_NtkDupObj( subNtk, pObj, 1 );
		
		if( Abc_ObjChild0Copy(pObj) == NULL)
		{
			Abc_ObjAddFanin( pObjNew, Abc_AigConst1(subNtk));
			pObjNew->fCompl0 = 1;
		}
		else if( Abc_ObjChild0Copy(pObj) == (void*)(1) )
		{
			Abc_ObjAddFanin( pObjNew, Abc_AigConst1(subNtk));
			pObjNew->fCompl0 = 0;
		}
		else
			Abc_ObjAddFanin( pObjNew, Abc_ObjChild0Copy(pObj) );
	}

	return subNtk;
}

FILE *matchFile;

int matchNonSingletonOutputs(Abc_Ntk_t * pNtk1, Vec_Ptr_t ** nodesInLevel1, Vec_Int_t ** iMatch1, Vec_Int_t ** iDep1, Vec_Int_t * matchedInputs1, int * iGroup1, Vec_Int_t ** oMatch1, int * oGroup1,
							  Abc_Ntk_t * pNtk2, Vec_Ptr_t ** nodesInLevel2, Vec_Int_t ** iMatch2, Vec_Int_t ** iDep2, Vec_Int_t * matchedInputs2, int * iGroup2, Vec_Int_t ** oMatch2, int * oGroup2,
							  Vec_Int_t * matchedOutputs1, Vec_Int_t * matchedOutputs2, Vec_Int_t * oMatchedGroups, Vec_Int_t * iNonSingleton,						 
							  Abc_Ntk_t * subNtk1, Abc_Ntk_t * subNtk2, Vec_Ptr_t * oMatchPairs,
							  Vec_Int_t * oNonSingleton, int oI, int idx, int ii, int iidx)
{		
	static int MATCH_FOUND;
	int i;
	int j, temp;
	Vec_Int_t * mismatch;		
	int * skipList;	
	static int counter = 0;

	MATCH_FOUND = FALSE;
	
	if( oI == Vec_IntSize( oNonSingleton ) )
	{
		if( iNonSingleton != NULL)			
			if( match1by1(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1,
				          pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2,
 					      matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton, ii, iidx) )
				MATCH_FOUND = TRUE;	

		if( iNonSingleton == NULL)
			MATCH_FOUND = TRUE;

		return MATCH_FOUND;
	}

	i = Vec_IntEntry(oNonSingleton, oI);

	mismatch = Vec_IntAlloc(10);
	
	skipList = ABC_ALLOC(int, Vec_IntSize(oMatch1[i]));

	for(j = 0; j < Vec_IntSize(oMatch1[i]); j++)
		skipList[j] = FALSE;

	Vec_PtrPush(oMatchPairs, Abc_NtkPo(subNtk1, Vec_IntEntry(oMatch1[i], idx)) );
	Vec_IntPush(matchedOutputs1, Vec_IntEntry(oMatch1[i], idx));

	for(j = 0; j < Vec_IntSize( oMatch2[i] ) && MATCH_FOUND == FALSE; j++)
	{
		if( Vec_IntEntry(oMatch2[i], j) == -1 || skipList[j] == TRUE)
			continue;

		Vec_PtrPush(oMatchPairs, Abc_NtkPo(subNtk2, Vec_IntEntry(oMatch2[i], j)));
		Vec_IntPush(matchedOutputs2, Vec_IntEntry(oMatch2[i], j));

		counter++;		
		if( Abc_NtkBmSat( subNtk1, subNtk2, NULL, oMatchPairs, mismatch, 0) )
		{
			/*fprintf(matchFile, "%s matched to %s\n", Abc_ObjName(Abc_NtkPo(pNtk1, Vec_IntEntry(oMatch1[i], idx))), 
										 Abc_ObjName(Abc_NtkPo(pNtk2, Vec_IntEntry(oMatch2[i], j))));			*/

			temp =  Vec_IntEntry(oMatch2[i], j);
			Vec_IntWriteEntry(oMatch2[i], j, -1);
			
			if(idx != Vec_IntSize( oMatch1[i] ) - 1)
				// call the same function with idx+1
				matchNonSingletonOutputs(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1,
										 pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2,
										 matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton,						 
										 subNtk1, subNtk2, oMatchPairs,
										 oNonSingleton, oI, idx+1, ii, iidx);
			else	
				// call the same function with idx = 0 and oI++
				matchNonSingletonOutputs(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1,
										 pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2,
										 matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton,						 
										 subNtk1, subNtk2, oMatchPairs,
										 oNonSingleton, oI+1, 0, ii, iidx);

			Vec_IntWriteEntry(oMatch2[i], j, temp);
		}		
		else
		{
			int * output1, * output2;
			int k;
			Abc_Obj_t * pObj;
			int * pModel;
			char * vPiValues;			
			

			vPiValues = ABC_ALLOC( char,  Abc_NtkPiNum(subNtk1) + 1);
			vPiValues[Abc_NtkPiNum(subNtk1)] = '\0';	
			
			for(k = 0; k < Abc_NtkPiNum(subNtk1); k++)
				vPiValues[k] = '0';

			for(k = 0; k < Vec_IntSize(mismatch); k += 2)			
				vPiValues[Vec_IntEntry(mismatch, k)] = Vec_IntEntry(mismatch, k+1);						

			pModel = ABC_ALLOC( int, Abc_NtkCiNum(subNtk1) );	

			Abc_NtkForEachPi( subNtk1, pObj, k )
				pModel[k] = vPiValues[k] - '0';
			Abc_NtkForEachLatch( subNtk1, pObj, k )
				pModel[Abc_NtkPiNum(subNtk1)+k] = pObj->iData - 1;			
	
			output1 = Abc_NtkVerifySimulatePattern( subNtk1, pModel );

			Abc_NtkForEachLatch( subNtk2, pObj, k )
				pModel[Abc_NtkPiNum(subNtk2)+k] = pObj->iData - 1;

			output2 = Abc_NtkVerifySimulatePattern( subNtk2, pModel );
			

			for(k = 0; k < Vec_IntSize( oMatch1[i] ); k++)
				if(output1[Vec_IntEntry(oMatch1[i], idx)] != output2[Vec_IntEntry(oMatch2[i], k)])
				{
					skipList[k] = TRUE;	
					/*printf("Output is SKIPPED");*/
				}
				
			ABC_FREE( vPiValues );
			ABC_FREE( pModel );
			ABC_FREE( output1 );
			ABC_FREE( output2 );
		}
		
		if(MATCH_FOUND == FALSE )
		{
			Vec_PtrPop(oMatchPairs);
			Vec_IntPop(matchedOutputs2);
		}
	}

	if(MATCH_FOUND == FALSE )
	{
		Vec_PtrPop(oMatchPairs);
		Vec_IntPop(matchedOutputs1);
	}

	if(MATCH_FOUND && counter != 0)
	{		
		/*printf("Number of OUTPUT SAT instances = %d", counter);*/
		counter = 0;
	}

	ABC_FREE( mismatch );
	ABC_FREE( skipList );

	return MATCH_FOUND;
}

int match1by1(Abc_Ntk_t * pNtk1, Vec_Ptr_t ** nodesInLevel1, Vec_Int_t ** iMatch1, Vec_Int_t ** iDep1, Vec_Int_t * matchedInputs1, int * iGroup1, Vec_Int_t ** oMatch1, int * oGroup1,
			   Abc_Ntk_t * pNtk2, Vec_Ptr_t ** nodesInLevel2, Vec_Int_t ** iMatch2, Vec_Int_t ** iDep2, Vec_Int_t * matchedInputs2, int * iGroup2, Vec_Int_t ** oMatch2, int * oGroup2,
			   Vec_Int_t * matchedOutputs1, Vec_Int_t * matchedOutputs2, Vec_Int_t * oMatchedGroups, Vec_Int_t * iNonSingleton, int ii, int idx)
{
	static int MATCH_FOUND = FALSE;
	Abc_Ntk_t * subNtk1, * subNtk2;
	Vec_Int_t * oNonSingleton;	
	Vec_Ptr_t * oMatchPairs;
	int * skipList;
	int j, m;	
	int i;		
	static int counter = 0;

	MATCH_FOUND = FALSE;

	if( ii == Vec_IntSize(iNonSingleton) )
	{
		MATCH_FOUND = TRUE;
		return TRUE;
	}
	
	i = Vec_IntEntry(iNonSingleton, ii);

	if( idx == Vec_IntSize(iMatch1[i]) )
	{		
		// call again with the next element in iNonSingleton
		return match1by1(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1,
				    	 pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2,
						 matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton, ii+1, 0);			
		
	}	
	
	oNonSingleton = Vec_IntAlloc(10);
	oMatchPairs = Vec_PtrAlloc(100);	
	skipList = ABC_ALLOC(int, Vec_IntSize(iMatch1[i]));

	for(j = 0; j < Vec_IntSize(iMatch1[i]); j++)
		skipList[j] = FALSE;
	
	Vec_IntPush(matchedInputs1, Vec_IntEntry(iMatch1[i], idx));
	idx++;
	
	if(idx == 1)
	{
		for(j = 0; j < Vec_IntSize(iDep1[Vec_IntEntryLast(iMatch1[i])]); j++)
		{
			if( Vec_IntSize(oMatch1[oGroup1[Vec_IntEntry(iDep1[Vec_IntEntryLast(iMatch1[i])], j)]]) == 1 ) 
				continue;
			if( Vec_IntFind( oMatchedGroups, oGroup1[Vec_IntEntry(iDep1[Vec_IntEntryLast(iMatch1[i])], j)]) != -1)
				continue;
			
			Vec_IntPushUnique(oNonSingleton,  oGroup1[Vec_IntEntry(iDep1[Vec_IntEntryLast(iMatch1[i])], j)]);
			Vec_IntPushUnique(oMatchedGroups, oGroup1[Vec_IntEntry(iDep1[Vec_IntEntryLast(iMatch1[i])], j)]);		
		}
	}

	subNtk1 = computeCofactor(pNtk1, nodesInLevel1, NULL, matchedInputs1);

	for(j = idx-1; j < Vec_IntSize(iMatch2[i]) && MATCH_FOUND == FALSE; j++)
	{
		int tempJ;
		Vec_Int_t * mismatch;

		if( skipList[j] )
			continue;

		mismatch = Vec_IntAlloc(10);

		Vec_IntPush(matchedInputs2, Vec_IntEntry(iMatch2[i], j));		
		
		subNtk2 = computeCofactor(pNtk2, nodesInLevel2, NULL, matchedInputs2);			

		for(m = 0; m < Vec_IntSize(matchedOutputs1); m++)
		{
			Vec_PtrPush(oMatchPairs, Abc_NtkPo(subNtk1, Vec_IntEntry(matchedOutputs1, m)));
			Vec_PtrPush(oMatchPairs, Abc_NtkPo(subNtk2, Vec_IntEntry(matchedOutputs2, m)));
		}

		counter++;

		if( Abc_NtkBmSat( subNtk2, subNtk1, NULL, oMatchPairs, mismatch, 0) )				
		{
			if(idx-1 != j)
			{
				tempJ = Vec_IntEntry(iMatch2[i], idx-1);
				Vec_IntWriteEntry(iMatch2[i], idx-1, Vec_IntEntry(iMatch2[i], j));
				Vec_IntWriteEntry(iMatch2[i], j, tempJ);
			}

			/*fprintf(matchFile, "%s matched to %s\n", Abc_ObjName(Abc_NtkPi(pNtk1, Vec_IntEntry(iMatch1[i], idx-1))), 
										    		  Abc_ObjName(Abc_NtkPi(pNtk2, Vec_IntEntry(iMatch2[i], j))));*/

			// we look for a match for outputs in oNonSingleton								
			matchNonSingletonOutputs(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1,
									 pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2,
									 matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton,						 
									 subNtk1, subNtk2, oMatchPairs, oNonSingleton, 0, 0, ii, idx);
			
			
			if(idx-1 != j)
			{
				tempJ = Vec_IntEntry(iMatch2[i], idx-1);
				Vec_IntWriteEntry(iMatch2[i], idx-1, Vec_IntEntry(iMatch2[i], j));
				Vec_IntWriteEntry(iMatch2[i], j, tempJ);
			}
		}
		else
		{
			Abc_Ntk_t * FpNtk1, * FpNtk2;
			int * bitVector1, * bitVector2;
			Vec_Int_t * currInputs1, * currInputs2;			
			Vec_Ptr_t * vSupp;	
			Abc_Obj_t * pObj;
			int suppNum1 = 0;
			int * suppNum2;			
			
			bitVector1 = ABC_ALLOC( int, Abc_NtkPiNum(pNtk1) );
			bitVector2 = ABC_ALLOC( int, Abc_NtkPiNum(pNtk2) );

			currInputs1 = Vec_IntAlloc(10);
			currInputs2 = Vec_IntAlloc(10);		
			
			suppNum2 = ABC_ALLOC(int, Vec_IntSize(iMatch2[i])-idx+1);

			for(m = 0; m < Abc_NtkPiNum(pNtk1); m++)
			{
				bitVector1[m] = 0;
				bitVector2[m] = 0;
			}

			for(m = 0; m < Vec_IntSize(iMatch2[i])-idx+1; m++)						
				suppNum2[m]= 0;			

			// First of all set the value of the inputs that are already matched and are in mismatch
			for(m = 0; m < Vec_IntSize(mismatch); m += 2)
			{
				int n = Vec_IntEntry(mismatch, m);
					
				bitVector1[Vec_IntEntry(matchedInputs1, n)] = Vec_IntEntry(mismatch, m+1);
				bitVector2[Vec_IntEntry(matchedInputs2, n)] = Vec_IntEntry(mismatch, m+1);
				
			}
			
			for(m = idx-1; m < Vec_IntSize(iMatch1[i]); m++)
			{
				Vec_IntPush(currInputs1, Vec_IntEntry(iMatch1[i], m));
				Vec_IntPush(currInputs2, Vec_IntEntry(iMatch2[i], m));
			}

			// Then add all the inputs that are not yet matched to the currInputs
			for(m = 0; m < Abc_NtkPiNum(pNtk1); m++)
			{
				if(Vec_IntFind( matchedInputs1, m ) == -1)
					Vec_IntPushUnique(currInputs1, m);

				if(Vec_IntFind( matchedInputs2, m ) == -1)
					Vec_IntPushUnique(currInputs2, m);
			}

			FpNtk1 = computeCofactor(pNtk1, nodesInLevel1, bitVector1, currInputs1);			
			FpNtk2 = computeCofactor(pNtk2, nodesInLevel2, bitVector2, currInputs2);    

			Abc_NtkForEachPo( FpNtk1, pObj, m )
			{		
				int n;
				vSupp  = Abc_NtkNodeSupport( FpNtk1, &pObj, 1 );			    		
				
				for(n = 0; n < vSupp->nSize; n++)
					if( Abc_ObjId((Abc_Obj_t *)vSupp->pArray[n]) == 1 )
						suppNum1 += Vec_IntFind( matchedOutputs1, m) + 1;				
						
				Vec_PtrFree( vSupp );
			}
			
			Abc_NtkForEachPo( FpNtk2, pObj, m )
			{		
				int n;
				vSupp  = Abc_NtkNodeSupport( FpNtk2, &pObj, 1 );			    		
				
				for(n = 0; n < vSupp->nSize; n++)
					if( (int)Abc_ObjId((Abc_Obj_t *)vSupp->pArray[n])-1 < (Vec_IntSize(iMatch2[i]))-idx+1 &&
						(int)Abc_ObjId((Abc_Obj_t *)vSupp->pArray[n])-1 >= 0)
						suppNum2[Abc_ObjId((Abc_Obj_t *)vSupp->pArray[n])-1] += Vec_IntFind( matchedOutputs2, m) + 1;				
						
				Vec_PtrFree( vSupp );
			}

			/*if(suppNum1 != 0)			
				printf("Ntk1 is trigged");			

			if(suppNum2[0] != 0)
				printf("Ntk2 is trigged");*/

			for(m = 0; m < Vec_IntSize(iMatch2[i])-idx+1; m++)
				if(suppNum2[m] != suppNum1)
				{
					skipList[m+idx-1] = TRUE;					
					/*printf("input is skipped");*/
				}
				
			Abc_NtkDelete( FpNtk1 );
			Abc_NtkDelete( FpNtk2 );
			ABC_FREE( bitVector1 );	
 			ABC_FREE( bitVector2 );	
			Vec_IntFree( currInputs1 );
			Vec_IntFree( currInputs2 );			
			ABC_FREE( suppNum2 );
		}
		
		Vec_PtrClear(oMatchPairs);
		Abc_NtkDelete( subNtk2 );
		Vec_IntFree(mismatch);

		//Vec_IntWriteEntry(iMatch2[i], j, tempJ);		
		
		if( MATCH_FOUND == FALSE )
			Vec_IntPop(matchedInputs2);
	}

	if( MATCH_FOUND == FALSE )
	{
		Vec_IntPop(matchedInputs1);	
		
		if(idx == 1)
		{
			for(m = 0; m < Vec_IntSize(oNonSingleton); m++)
				Vec_IntPop( oMatchedGroups );
		}
	}
	
	Vec_IntFree( oNonSingleton );	
	Vec_PtrFree( oMatchPairs );	
	ABC_FREE( skipList );
	Abc_NtkDelete( subNtk1 );	

	if(MATCH_FOUND && counter != 0)
	{		
		/*printf("Number of INPUT SAT instances = %d\n", counter);*/

		counter = 0;
	}

	return MATCH_FOUND;
}

float refineBySAT(Abc_Ntk_t * pNtk1, Vec_Int_t ** iMatch1, int * iGroup1, Vec_Int_t ** iDep1, int* iLastItem1, Vec_Int_t ** oMatch1, int * oGroup1, Vec_Int_t ** oDep1, int* oLastItem1, int * observability1,
				 Abc_Ntk_t * pNtk2, Vec_Int_t ** iMatch2, int * iGroup2, Vec_Int_t ** iDep2, int* iLastItem2, Vec_Int_t ** oMatch2, int * oGroup2, Vec_Int_t ** oDep2, int* oLastItem2, int * observability2)
{
	int i, j;	
	Abc_Obj_t * pObj;
	Vec_Int_t * iNonSingleton;
	Vec_Int_t * matchedInputs1, * matchedInputs2;
	Vec_Int_t * matchedOutputs1, * matchedOutputs2;
	Vec_Ptr_t ** nodesInLevel1, ** nodesInLevel2;
	Vec_Int_t * oMatchedGroups;
	FILE *result;	
	int matchFound;
	abctime clk = Abc_Clock();
	float satTime = 0.0;

	/*matchFile = fopen("satmatch.txt", "w");*/
	
	iNonSingleton = Vec_IntAlloc(10);	
	
	matchedInputs1 = Vec_IntAlloc( Abc_NtkPiNum(pNtk1) );
	matchedInputs2 = Vec_IntAlloc( Abc_NtkPiNum(pNtk2) );

	matchedOutputs1 = Vec_IntAlloc( Abc_NtkPoNum(pNtk1) );
	matchedOutputs2 = Vec_IntAlloc( Abc_NtkPoNum(pNtk2) );

	nodesInLevel1 = ABC_ALLOC( Vec_Ptr_t *, Abc_AigLevel( pNtk1 ) + 1);	// why numOfLevels+1? because the inputs are in level 0
	for(i = 0; i <= Abc_AigLevel( pNtk1 ); i++)
		nodesInLevel1[i] = Vec_PtrAlloc( 20 );

	// bucket sort the objects based on their levels
	Abc_AigForEachAnd( pNtk1, pObj, i )	
		Vec_PtrPush(nodesInLevel1[Abc_ObjLevel(pObj)], pObj);
	
	nodesInLevel2 = ABC_ALLOC( Vec_Ptr_t *, Abc_AigLevel( pNtk2 ) + 1);	// why numOfLevels+1? because the inputs are in level 0
	for(i = 0; i <= Abc_AigLevel( pNtk2 ); i++)
		nodesInLevel2[i] = Vec_PtrAlloc( 20 );

	// bucket sort the objects based on their levels
	Abc_AigForEachAnd( pNtk2, pObj, i )	
		Vec_PtrPush(nodesInLevel2[Abc_ObjLevel(pObj)], pObj);	

	oMatchedGroups = Vec_IntAlloc( 10 );

	for(i = 0; i < *iLastItem1; i++)
	{
		if(Vec_IntSize(iMatch1[i]) == 1)
		{
			Vec_IntPush(matchedInputs1, Vec_IntEntryLast(iMatch1[i]));
			Vec_IntPush(matchedInputs2, Vec_IntEntryLast(iMatch2[i]));		
		}
		else
			Vec_IntPush(iNonSingleton, i);
	}

	for(i = 0; i < *oLastItem1; i++)
	{
		if(Vec_IntSize(oMatch1[i]) == 1)
		{
			Vec_IntPush(matchedOutputs1, Vec_IntEntryLast(oMatch1[i]));
			Vec_IntPush(matchedOutputs2, Vec_IntEntryLast(oMatch2[i]));
		}
	}
	
	for(i = 0; i < Vec_IntSize(iNonSingleton) - 1; i++)
	{
		for(j = i + 1; j < Vec_IntSize(iNonSingleton); j++)		
			if( observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, j)], 0)] > 
				observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, i)], 0)] )
			{				
				int temp = Vec_IntEntry(iNonSingleton, i);
				Vec_IntWriteEntry( iNonSingleton, i, Vec_IntEntry(iNonSingleton, j) );
				Vec_IntWriteEntry( iNonSingleton, j, temp );				
			}
			else if( observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, j)], 0)] == 
					 observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, i)], 0)] )
			{
				if( Vec_IntSize(iMatch2[Vec_IntEntry(iNonSingleton, j)]) < Vec_IntSize(iMatch2[Vec_IntEntry(iNonSingleton, i)]) )
				{
					int temp = Vec_IntEntry(iNonSingleton, i);
					Vec_IntWriteEntry( iNonSingleton, i, Vec_IntEntry(iNonSingleton, j) );
					Vec_IntWriteEntry( iNonSingleton, j, temp );				
				}
			}
	}	

	/*for(i = 0; i < Vec_IntSize(iNonSingleton) - 1; i++)
	{
		for(j = i + 1; j < Vec_IntSize(iNonSingleton); j++)		
			if( Vec_IntSize(oDep2[oGroup2[Vec_IntEntryLast(iMatch2[Vec_IntEntry(iNonSingleton, j)])]]) > 
				Vec_IntSize(oDep2[oGroup2[Vec_IntEntryLast(iMatch2[Vec_IntEntry(iNonSingleton, i)])]]) )
			{				
				int temp = Vec_IntEntry(iNonSingleton, i);
				Vec_IntWriteEntry( iNonSingleton, i, Vec_IntEntry(iNonSingleton, j) );
				Vec_IntWriteEntry( iNonSingleton, j, temp );				
			}
			else if( Vec_IntSize(oDep2[oGroup2[Vec_IntEntryLast(iMatch2[Vec_IntEntry(iNonSingleton, j)])]]) == 
				Vec_IntSize(oDep2[oGroup2[Vec_IntEntryLast(iMatch2[Vec_IntEntry(iNonSingleton, i)])]]) )
			{
				if( observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, j)], 0)] > 
						observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, i)], 0)] )
				{
					int temp = Vec_IntEntry(iNonSingleton, i);
					Vec_IntWriteEntry( iNonSingleton, i, Vec_IntEntry(iNonSingleton, j) );
					Vec_IntWriteEntry( iNonSingleton, j, temp );				
				}
			}
	}*/

	matchFound = match1by1(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1,
						   pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2,
						   matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton, 0, 0);

	if( matchFound && Vec_IntSize(matchedOutputs1) != Abc_NtkPoNum(pNtk1) )
	{
		Vec_Int_t * oNonSingleton;
		Vec_Ptr_t * oMatchPairs;
		Abc_Ntk_t * subNtk1, * subNtk2;

		oNonSingleton = Vec_IntAlloc( 10 );
		
		oMatchPairs = Vec_PtrAlloc(Abc_NtkPoNum(pNtk1) * 2);	

		for(i = 0; i < *oLastItem1; i++)
			if( Vec_IntSize(oMatch1[i]) > 1 && Vec_IntFind( oMatchedGroups, i) == -1 )
				Vec_IntPush(oNonSingleton, i);
			
		subNtk1 = computeCofactor(pNtk1, nodesInLevel1, NULL, matchedInputs1);
		subNtk2 = computeCofactor(pNtk2, nodesInLevel2, NULL, matchedInputs2);
		
		matchFound = matchNonSingletonOutputs(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1,
								 pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup1, oMatch2, oGroup2,
								 matchedOutputs1, matchedOutputs2, oMatchedGroups, NULL,						 
								 subNtk1, subNtk2, oMatchPairs, oNonSingleton, 0, 0, 0, 0);

		Vec_IntFree( oNonSingleton );		
		Vec_PtrFree( oMatchPairs );

		Abc_NtkDelete(subNtk1);
		Abc_NtkDelete(subNtk2);
	}

	satTime = (float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC);	

	if( matchFound )
	{
  		checkEquivalence( pNtk1, matchedInputs1, matchedOutputs1, pNtk2, matchedInputs2, matchedOutputs2);

		result = fopen("IOmatch.txt", "w");

		fprintf(result, "I/O = %d / %d \n\n", Abc_NtkPiNum(pNtk1), Abc_NtkPoNum(pNtk1));
		
		for(i = 0; i < Vec_IntSize(matchedInputs1) ; i++)
  			fprintf(result, "{%s}\t{%s}\n", Abc_ObjName(Abc_NtkPi(pNtk1, Vec_IntEntry(matchedInputs1, i))), Abc_ObjName(Abc_NtkPi(pNtk2, Vec_IntEntry(matchedInputs2, i))) );									

		fprintf(result, "\n-----------------------------------------\n");

		for(i = 0; i < Vec_IntSize(matchedOutputs1) ; i++)
			fprintf(result, "{%s}\t{%s}\n", Abc_ObjName(Abc_NtkPo(pNtk1, Vec_IntEntry(matchedOutputs1, i))), Abc_ObjName(Abc_NtkPo(pNtk2, Vec_IntEntry(matchedOutputs2, i))) );									

		fclose( result );	
	}

	Vec_IntFree( matchedInputs1 );
	Vec_IntFree( matchedInputs2 );
	Vec_IntFree( matchedOutputs1 );
	Vec_IntFree( matchedOutputs2 );
	Vec_IntFree( iNonSingleton );
	Vec_IntFree( oMatchedGroups );
	
	for(i = 0; i <= Abc_AigLevel( pNtk1 ); i++)	
		Vec_PtrFree( nodesInLevel1[i] );
	for(i = 0; i <= Abc_AigLevel( pNtk2 ); i++)	
		Vec_PtrFree( nodesInLevel2[i] );
	

	ABC_FREE( nodesInLevel1 );
	ABC_FREE( nodesInLevel2 );
	/*fclose(matchFile);*/
	
	return satTime;
}

int checkListConsistency(Vec_Int_t ** iMatch1, Vec_Int_t ** oMatch1, Vec_Int_t ** iMatch2, Vec_Int_t ** oMatch2, int iLastItem1, int oLastItem1, int iLastItem2, int oLastItem2)
{
	//int i;

	if(iLastItem1 != iLastItem2 || oLastItem1 != oLastItem2)
		return FALSE;

	/*for(i = 0; i < iLastItem1; i++) {
		if(Vec_IntSize(iMatch1[i]) != Vec_IntSize(iMatch2[i]))
			return FALSE;
	}

	for(i = 0; i < oLastItem1; i++) {
		if(Vec_IntSize(oMatch1[i]) != Vec_IntSize(oMatch2[i]))
			return FALSE;
	}*/
		
	return TRUE;
}


void bmGateWay( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int p_equivalence )
{	
	Vec_Int_t ** iDep1, ** oDep1;
	Vec_Int_t ** iDep2, ** oDep2;
	Vec_Int_t ** iMatch1, ** oMatch1;
	Vec_Int_t ** iMatch2, ** oMatch2;		
	int * iGroup1, * oGroup1;
	int * iGroup2, * oGroup2;
	int iLastItem1, oLastItem1;
	int iLastItem2, oLastItem2;	
	int i, j;	
	
	char * vPiValues1, * vPiValues2;
	int * observability1, * observability2;
	abctime clk = Abc_Clock();
	float initTime;
	float simulTime;
	float satTime;
	Vec_Ptr_t ** topOrder1 = NULL, ** topOrder2 = NULL;

	extern void getDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep);
	extern void initMatchList(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep, Vec_Int_t** iMatch, int* iLastItem, Vec_Int_t** oMatch, int* oLastItem, int* iGroup, int* oGroup, int p_equivalence);		
	extern void iSortDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, int* oGroup);
	extern void oSortDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** oDep, int* iGroup);
	extern int iSplitByDep(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** iMatch, int* iGroup, int* iLastItem, int* oGroup);
	extern int oSplitByDep(Abc_Ntk_t *pNtk, Vec_Int_t** oDep, Vec_Int_t** oMatch, int* oGroup, int* oLastItem, int* iGroup);	
	extern Vec_Ptr_t ** findTopologicalOrder(Abc_Ntk_t * pNtk);
	extern int refineIOBySimulation(Abc_Ntk_t *pNtk, Vec_Int_t** iMatch, int* iLastItem, int * iGroup, Vec_Int_t** iDep, Vec_Int_t** oMatch, int* oLastItem, int * oGroup, Vec_Int_t** oDep, char * vPiValues, int * observability, Vec_Ptr_t ** topOrder);	
	extern float refineBySAT(Abc_Ntk_t * pNtk1, Vec_Int_t ** iMatch1, int * iGroup1, Vec_Int_t ** iDep1, int* iLastItem1, Vec_Int_t ** oMatch1, int * oGroup1, Vec_Int_t ** oDep1, int* oLastItem1, int * observability1,
							Abc_Ntk_t * pNtk2, Vec_Int_t ** iMatch2, int * iGroup2, Vec_Int_t ** iDep2, int* iLastItem2, Vec_Int_t ** oMatch2, int * oGroup2, Vec_Int_t ** oDep2, int* oLastItem2, int * observability2);				
	int checkListConsistency(Vec_Int_t ** iMatch1, Vec_Int_t ** oMatch1, Vec_Int_t ** iMatch2, Vec_Int_t ** oMatch2, int iLastItem1, int oLastItem1, int iLastItem2, int oLastItem2);	

	iDep1 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPiNum(pNtk1) );
	oDep1 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPoNum(pNtk1) );

	iDep2 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPiNum(pNtk2) );
	oDep2 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPoNum(pNtk2) );

	iMatch1 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPiNum(pNtk1) );
	oMatch1 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPoNum(pNtk1) );

	iMatch2 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPiNum(pNtk2) );
	oMatch2 = ABC_ALLOC( Vec_Int_t*,  (unsigned)Abc_NtkPoNum(pNtk2) );		

	iGroup1 = ABC_ALLOC( int, Abc_NtkPiNum(pNtk1) );
	oGroup1 = ABC_ALLOC( int, Abc_NtkPoNum(pNtk1) );

	iGroup2 = ABC_ALLOC( int, Abc_NtkPiNum(pNtk2) );
	oGroup2 = ABC_ALLOC( int, Abc_NtkPoNum(pNtk2) );

	vPiValues1 = ABC_ALLOC( char,  Abc_NtkPiNum(pNtk1) + 1);
	vPiValues1[Abc_NtkPiNum(pNtk1)] = '\0';	

	vPiValues2 = ABC_ALLOC( char,  Abc_NtkPiNum(pNtk2) + 1);
	vPiValues2[Abc_NtkPiNum(pNtk2)] = '\0';	

	observability1 = ABC_ALLOC(int, (unsigned)Abc_NtkPiNum(pNtk1));
	observability2 = ABC_ALLOC(int, (unsigned)Abc_NtkPiNum(pNtk2));

	for(i = 0; i < Abc_NtkPiNum(pNtk1); i++)
	{		
		iDep1[i] = Vec_IntAlloc( 1 );
		iMatch1[i] = Vec_IntAlloc( 1 );

		iDep2[i] = Vec_IntAlloc( 1 );
		iMatch2[i] = Vec_IntAlloc( 1 );

		vPiValues1[i] = '0';
		vPiValues2[i] = '0';

		observability1[i] = 0;
		observability2[i] = 0;
	}

	for(i = 0; i < Abc_NtkPoNum(pNtk1); i++)
	{
		oDep1[i] = Vec_IntAlloc( 1 );
		oMatch1[i] = Vec_IntAlloc( 1 );

		oDep2[i] = Vec_IntAlloc( 1 );
		oMatch2[i] = Vec_IntAlloc( 1 );
	}	
	
	/************* Strashing ************/	
	pNtk1 = Abc_NtkStrash( pNtk1, 0, 0, 0 );	
	pNtk2 = Abc_NtkStrash( pNtk2, 0, 0, 0 );			
	printf("Network  strashing is done!\n");	
	/************************************/	
	
	/******* Getting Dependencies *******/	
	getDependencies(pNtk1, iDep1, oDep1);
	getDependencies(pNtk2, iDep2, oDep2);			
	printf("Getting dependencies is done!\n");	
	/************************************/

	/***** Intializing match lists ******/	
	initMatchList(pNtk1, iDep1, oDep1, iMatch1, &iLastItem1, oMatch1, &oLastItem1, iGroup1, oGroup1, p_equivalence);			
	initMatchList(pNtk2, iDep2, oDep2, iMatch2, &iLastItem2, oMatch2, &oLastItem2, iGroup2, oGroup2, p_equivalence);	
	printf("Initializing match lists is done!\n");		
	/************************************/

	if( !checkListConsistency(iMatch1, oMatch1, iMatch2, oMatch2, iLastItem1, oLastItem1, iLastItem2, oLastItem2) )
	{
		fprintf( stdout, "I/O dependencies of two circuits are different.\n");
		goto freeAndExit;
	}		

	printf("Refining IOs by dependencies ...");				
	// split match lists further by checking dependencies
	do
	{
		int iNumOfItemsAdded = 1, oNumOfItemsAdded = 1;		

		do
		{	
			if( oNumOfItemsAdded )
			{
				iSortDependencies(pNtk1, iDep1, oGroup1);
				iSortDependencies(pNtk2, iDep2, oGroup2);
			}
			
			if( iNumOfItemsAdded )
			{
				oSortDependencies(pNtk1, oDep1, iGroup1);
				oSortDependencies(pNtk2, oDep2, iGroup2);
			}

			if( iLastItem1 < Abc_NtkPiNum(pNtk1) )
			{				
				iSplitByDep(pNtk1, iDep1, iMatch1, iGroup1, &iLastItem1, oGroup1);
				if( oLastItem1 < Abc_NtkPoNum(pNtk1) )
					oSplitByDep(pNtk1, oDep1, oMatch1, oGroup1, &oLastItem1, iGroup1);
			}				

			if( iLastItem2 < Abc_NtkPiNum(pNtk2) )
			{				
				iNumOfItemsAdded = iSplitByDep(pNtk2, iDep2, iMatch2, iGroup2, &iLastItem2, oGroup2);
				if( oLastItem2 < Abc_NtkPoNum(pNtk2) )		
					oNumOfItemsAdded = oSplitByDep(pNtk2, oDep2, oMatch2, oGroup2, &oLastItem2, iGroup2);
				else
					oNumOfItemsAdded = 0;
			}
			else
				iNumOfItemsAdded = 0;							
			
			if(!checkListConsistency(iMatch1, oMatch1, iMatch2, oMatch2, iLastItem1, oLastItem1, iLastItem2, oLastItem2))
			{
				fprintf( stdout, "I/O dependencies of two circuits are different.\n");
				goto freeAndExit;
			}		
		}while(iNumOfItemsAdded != 0 || oNumOfItemsAdded != 0);

	}while(0);

	printf(" done!\n");

	initTime = ((float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC));	
	clk = Abc_Clock();

	topOrder1 = findTopologicalOrder(pNtk1);
	topOrder2 = findTopologicalOrder(pNtk2);

	printf("Refining IOs by simulation ...");				

	do
	{
		int counter = 0;
		int ioSuccess1, ioSuccess2;	
		
		do
		{
			for(i = 0; i < iLastItem1; i++)
			{
				int temp = (int)(SIM_RANDOM_UNSIGNED % 2);		
				
				if(Vec_IntSize(iMatch1[i]) != Vec_IntSize(iMatch2[i]))
				{
					fprintf( stdout, "Input refinement by simulation finds two circuits different.\n");				
					goto freeAndExit;
				}
				
				for(j = 0; j < Vec_IntSize(iMatch1[i]); j++)
				{
					vPiValues1[Vec_IntEntry(iMatch1[i], j)] = temp + '0';
					vPiValues2[Vec_IntEntry(iMatch2[i], j)] = temp + '0';	
				}			
			}					
			
			ioSuccess1 = refineIOBySimulation(pNtk1, iMatch1, &iLastItem1, iGroup1, iDep1, oMatch1, &oLastItem1, oGroup1, oDep1, vPiValues1, observability1, topOrder1);				
			ioSuccess2 = refineIOBySimulation(pNtk2, iMatch2, &iLastItem2, iGroup2, iDep2, oMatch2, &oLastItem2, oGroup2, oDep2, vPiValues2, observability2, topOrder2);
			
			if(ioSuccess1 && ioSuccess2)
				counter = 0;
			else
				counter++;						
			
			if(ioSuccess1 != ioSuccess2 ||
			   !checkListConsistency(iMatch1, oMatch1, iMatch2, oMatch2, iLastItem1, oLastItem1, iLastItem2, oLastItem2))
			{
				fprintf( stdout, "Input refinement by simulation finds two circuits different.\n");				
				goto freeAndExit;
			}
		}while(counter <= 200);				
		
	}while(0);	

	printf(" done!\n");
	
	simulTime = (float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC);
	printf("SAT-based search started ...\n");

	satTime = refineBySAT(pNtk1, iMatch1, iGroup1, iDep1, &iLastItem1, oMatch1, oGroup1, oDep1, &oLastItem1, observability1,
		   					   pNtk2, iMatch2, iGroup2, iDep2, &iLastItem2, oMatch2, oGroup2, oDep2, &oLastItem2, observability2);

	printf( "Init Time = %4.2f\n", initTime );	
	printf( "Simulation Time = %4.2f\n", simulTime );
	printf( "SAT Time = %4.2f\n", satTime );
	printf( "Overall Time = %4.2f\n", initTime + simulTime + satTime );
	
freeAndExit:

	for(i = 0; i < iLastItem1 ; i++)
	{			
		
		Vec_IntFree( iMatch1[i] );
		Vec_IntFree( iMatch2[i] );
	}
	
	for(i = 0; i < oLastItem1 ; i++)
	{			
		
		Vec_IntFree( oMatch1[i] );
		Vec_IntFree( oMatch2[i] );
	}

	for(i = 0; i < Abc_NtkPiNum(pNtk1); i++)
	{
		Vec_IntFree( iDep1[i] );
		Vec_IntFree( iDep2[i] );
		if(topOrder1 != NULL) {
			Vec_PtrFree( topOrder1[i] );
			Vec_PtrFree( topOrder2[i] );
		}
	}

	for(i = 0; i < Abc_NtkPoNum(pNtk1); i++)
	{
		Vec_IntFree( oDep1[i] );
		Vec_IntFree( oDep2[i] );
	}

	ABC_FREE( iMatch1 );
	ABC_FREE( iMatch2 );
	ABC_FREE( oMatch1 );
	ABC_FREE( oMatch2 );
	ABC_FREE( iDep1 );
	ABC_FREE( iDep2 );
	ABC_FREE( oDep1 );
	ABC_FREE( oDep2 );
	ABC_FREE( iGroup1 );
	ABC_FREE( iGroup2 );
	ABC_FREE( oGroup1 );
	ABC_FREE( oGroup2 );	
	ABC_FREE( vPiValues1 );
	ABC_FREE( vPiValues2 );
	ABC_FREE( observability1 );
	ABC_FREE( observability2 );
	if(topOrder1 != NULL) {
		ABC_FREE( topOrder1 );
		ABC_FREE( topOrder2 );
	}
}ABC_NAMESPACE_IMPL_END