abcBm.c File Reference

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

Go to the source code of this file.

Functions
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)
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)
void	iSortDependencies (Abc_Ntk_t *pNtk, Vec_Int_t **iDep, int *oGroup)
void	oSortDependencies (Abc_Ntk_t *pNtk, Vec_Int_t **oDep, int *iGroup)
int	oSplitByDep (Abc_Ntk_t *pNtk, Vec_Int_t **oDep, Vec_Int_t **oMatch, int *oGroup, int *oLastItem, int *iGroup)
int	iSplitByDep (Abc_Ntk_t *pNtk, Vec_Int_t **iDep, Vec_Int_t **iMatch, int *iGroup, int *iLastItem, int *oGroup)
Vec_Ptr_t **	findTopologicalOrder (Abc_Ntk_t *pNtk)
int *	Abc_NtkSimulateOneNode (Abc_Ntk_t *pNtk, int *pModel, int input, Vec_Ptr_t **topOrder)
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_Ntk_t *	Abc_NtkMiterBm (Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, Vec_Ptr_t *iCurrMatch, Vec_Ptr_t *oCurrMatch)
void	Abc_NtkVerifyReportError (Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int *pModel, Vec_Int_t *mismatch)
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)
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)
Abc_Ntk_t *	computeCofactor (Abc_Ntk_t *pNtk, Vec_Ptr_t **nodesInLevel, int *bitVector, Vec_Int_t *currInputs)
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)
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)
void	bmGateWay (Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int p_equivalence)

Variables
int *	pValues1__
int *	pValues2__
FILE *	matchFile

Function Documentation

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
	)

Definition at line 965 of file abcBm.c.

{    
    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;
}

Abc_Ntk_t* Abc_NtkMiterBm	(	Abc_Ntk_t *	pNtk1,
		Abc_Ntk_t *	pNtk2,
		Vec_Ptr_t *	iCurrMatch,
		Vec_Ptr_t *	oCurrMatch
	)

Definition at line 698 of file abcBm.c.

{
    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 Abc_NtkMiterSatBm	(	Abc_Ntk_t *	pNtk,
		ABC_INT64_T	nConfLimit,
		ABC_INT64_T	nInsLimit,
		int	fVerbose,
		ABC_INT64_T *	pNumConfs,
		ABC_INT64_T *	pNumInspects
	)

Definition at line 869 of file abcBm.c.

{
    static sat_solver * pSat = NULL;
    lbool   status;
    int RetValue;
    abctime clk;    

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

    assert( Abc_NtkLatchNum(pNtk) == 0 );

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

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

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

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

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

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

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

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

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

int* Abc_NtkSimulateOneNode	(	Abc_Ntk_t *	pNtk,
		int *	pModel,
		int	input,
		Vec_Ptr_t **	topOrder
	)

Definition at line 447 of file abcBm.c.

{
    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;
}

void Abc_NtkVerifyReportError	(	Abc_Ntk_t *	pNtk1,
		Abc_Ntk_t *	pNtk2,
		int *	pModel,
		Vec_Int_t *	mismatch
	)

Definition at line 808 of file abcBm.c.

{
    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__ );
}

void bmGateWay	(	Abc_Ntk_t *	pNtk1,
		Abc_Ntk_t *	pNtk2,
		int	p_equivalence
	)

Definition at line 1777 of file abcBm.c.

{   
    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

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
	)

Definition at line 1061 of file abcBm.c.

{   
    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;
}

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
	)

Definition at line 1756 of file abcBm.c.

{
    //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;
}

Abc_Ntk_t* computeCofactor	(	Abc_Ntk_t *	pNtk,
		Vec_Ptr_t **	nodesInLevel,
		int *	bitVector,
		Vec_Int_t *	currInputs
	)

Definition at line 1097 of file abcBm.c.

{   
    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;
}

static Vec_Ptr_t ** findTopologicalOrder

(

Abc_Ntk_t *

pNtk

)

Definition at line 420 of file abcBm.c.

{
    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;
}

static void getDependencies	(	Abc_Ntk_t *	pNtk,
		Vec_Int_t **	iDep,
		Vec_Int_t **	oDep
	)

Definition at line 44 of file abcBm.c.

{   
    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
	)

Definition at line 101 of file abcBm.c.

{
    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
	)

Definition at line 199 of file abcBm.c.

{
    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 );
}

int iSplitByDep	(	Abc_Ntk_t *	pNtk,
		Vec_Int_t **	iDep,
		Vec_Int_t **	iMatch,
		int *	iGroup,
		int *	iLastItem,
		int *	oGroup
	)

Definition at line 354 of file abcBm.c.

{
    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; 
}

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
	)

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.nosp@m.@umi.nosp@m.ch.ed.nosp@m.u.] [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.]

Definition at line 1329 of file abcBm.c.

{
    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;
}

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
	)

Definition at line 1183 of file abcBm.c.

{       
    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;
}

void oSortDependencies	(	Abc_Ntk_t *	pNtk,
		Vec_Int_t **	oDep,
		int *	iGroup
	)

Definition at line 241 of file abcBm.c.

{
    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
	)

Definition at line 283 of file abcBm.c.

{
    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;
}

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
	)

Definition at line 1574 of file abcBm.c.

{
    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 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
	)

Definition at line 508 of file abcBm.c.

{
    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;   
}

Variable Documentation

FILE* matchFile

Definition at line 1181 of file abcBm.c.

int* pValues1__

Definition at line 806 of file abcBm.c.

int * pValues2__

Definition at line 806 of file abcBm.c.