initial commit of public abc

1 files changed, 2047 insertions, 0 deletions

diff --git a/src/base/abci/abcBm.c b/src/base/abci/abcBm.c
new file mode 100644
index 00000000..8855fd9e
--- /dev/null
+++ b/src/base/abci/abcBm.c
@@ -0,0 +1,2047 @@
+/**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 "abc.h"
+#include "sim.h"
+#include "satSolver.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->pCopy = (Abc_Obj_t *)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->pCopy != (Abc_Obj_t *)(Value0 & Value1))
+        {
+            pNode->pCopy = (Abc_Obj_t *)(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->pCopy = (Abc_Obj_t *)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, 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 = 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", clock() - clk );
+
+    // simplify the problem
+    clk = 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", clock() - clk );
+    if ( status == 0 )
+    {
+        sat_solver_delete( pSat );
+//        printf( "The problem is UNSATISFIABLE after simplification.\n" );
+        return 1;
+    }
+
+    // solve the miter
+    clk = 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", 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( Abc_ObjId((Abc_Obj_t *)vSupp->pArray[n])-1 < (unsigned)(Vec_IntSize(iMatch2[i]))-idx+1 &&
+                        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;
+    int clk = 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)(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;
+    int clk = 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)(clock() - clk)/(float)(CLOCKS_PER_SEC));    
+    clk = 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)(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
+