/**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 "bdd/extrab/extraBdd.h"

ABC_NAMESPACE_IMPL_START

#define FALSE 0
#define TRUE  1

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 = 0;
    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 = 0;

    // 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);
            else
                iNumOfItemsAdded = 0;    
                
            if( oLastItem2 < Abc_NtkPoNum(pNtk2) )        
                oNumOfItemsAdded = oSplitByDep(pNtk2, oDep2, oMatch2, oGroup2, &oLastItem2, iGroup2);
            else
                oNumOfItemsAdded = 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