自学教程：C++ ABC_FREE函数代码示例

/**Function*************************************************************  Synopsis    [Gets the tokens taking into account the line breaks.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/Vec_Ptr_t * Io_ReadBlifGetTokens( Io_ReadBlif_t * p ){    Vec_Ptr_t * vTokens;    char * pLastToken;    int i;    // get rid of the old tokens    if ( p->vNewTokens->nSize > 0 )    {        for ( i = 0; i < p->vNewTokens->nSize; i++ )            ABC_FREE( p->vNewTokens->pArray[i] );        p->vNewTokens->nSize = 0;    }    // get the new tokens    vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p->pReader);    if ( vTokens == NULL )        return vTokens;    // check if there is a transfer to another line    pLastToken = (char *)vTokens->pArray[vTokens->nSize - 1];    if ( pLastToken[ strlen(pLastToken)-1 ] != '//' )        return vTokens;    // remove the slash    pLastToken[ strlen(pLastToken)-1 ] = 0;    if ( pLastToken[0] == 0 )        vTokens->nSize--;    // load them into the new array    for ( i = 0; i < vTokens->nSize; i++ )        Vec_PtrPush( p->vNewTokens, Extra_UtilStrsav((char *)vTokens->pArray[i]) );    // load as long as there is the line break    while ( 1 )    {        // get the new tokens        vTokens = (Vec_Ptr_t *)Extra_FileReaderGetTokens(p->pReader);        if ( vTokens->nSize == 0 )            return p->vNewTokens;        // check if there is a transfer to another line        pLastToken = (char *)vTokens->pArray[vTokens->nSize - 1];        if ( pLastToken[ strlen(pLastToken)-1 ] == '//' )        {            // remove the slash            pLastToken[ strlen(pLastToken)-1 ] = 0;            if ( pLastToken[0] == 0 )                vTokens->nSize--;            // load them into the new array            for ( i = 0; i < vTokens->nSize; i++ )                Vec_PtrPush( p->vNewTokens, Extra_UtilStrsav((char *)vTokens->pArray[i]) );            continue;        }        // otherwise, load them and break        for ( i = 0; i < vTokens->nSize; i++ )            Vec_PtrPush( p->vNewTokens, Extra_UtilStrsav((char *)vTokens->pArray[i]) );        break;    }    return p->vNewTokens;}

/**Function********************************************************************  Synopsis    [Creates the symmetry information structure from ZDD.]  Description [ZDD representation of symmetries is the set of cubes, each  of which has two variables in the positive polarity. These variables correspond  to the symmetric variable pair.]  SideEffects []  SeeAlso     []******************************************************************************/Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bSupp ){    int i;    int nSuppSize;    Extra_SymmInfo_t * p;    int * pMapVars2Nums;    DdNode * bTemp;    DdNode * zSet, * zCube, * zTemp;    int iVar1, iVar2;    nSuppSize = Extra_bddSuppSize( dd, bSupp );    // allocate and clean the storage for symmetry info    p = Extra_SymmPairsAllocate( nSuppSize );    // allocate the storage for the temporary map    pMapVars2Nums = ABC_ALLOC( int, dd->size );    memset( pMapVars2Nums, 0, dd->size * sizeof(int) );    // assign the variables    p->nVarsMax = dd->size;//  p->nNodes   = Cudd_DagSize( zPairs );    p->nNodes   = 0;    for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )    {        p->pVars[i] = bTemp->index;        pMapVars2Nums[bTemp->index] = i;    }    // write the symmetry info into the structure    zSet = zPairs;   Cudd_Ref( zSet );    while ( zSet != z0 )    {        // get the next cube        zCube  = Extra_zddSelectOneSubset( dd, zSet );    Cudd_Ref( zCube );        // add these two variables to the data structure        assert( cuddT( cuddT(zCube) ) == z1 );        iVar1 = zCube->index/2;        iVar2 = cuddT(zCube)->index/2;        if ( pMapVars2Nums[iVar1] < pMapVars2Nums[iVar2] )            p->pSymms[ pMapVars2Nums[iVar1] ][ pMapVars2Nums[iVar2] ] = 1;        else            p->pSymms[ pMapVars2Nums[iVar2] ][ pMapVars2Nums[iVar1] ] = 1;        // count the symmetric pairs        p->nSymms ++;        // update the cuver and deref the cube        zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube );     Cudd_Ref( zSet );        Cudd_RecursiveDerefZdd( dd, zTemp );        Cudd_RecursiveDerefZdd( dd, zCube );    } // for each cube     Cudd_RecursiveDerefZdd( dd, zSet );    ABC_FREE( pMapVars2Nums );    return p;} /* end of Extra_SymmPairsCreateFromZdd */

/**Function********************************************************************  Synopsis    [Annotates every node in the BDD node with its minterm count.]  Description [Annotates every node in the BDD node with its minterm count.  In this function, every node and the minterm count represented by it are  stored in a hash table.]  SideEffects [Fills up 'table' with the pair <node,minterm_count>.]******************************************************************************/static doublebddAnnotateMintermCount(  DdManager * manager,  DdNode * node,  double  max,  st_table * table){    DdNode *N,*Nv,*Nnv;    register double min_v,min_nv;    register double min_N;    double *pmin;    double *dummy;    statLine(manager);    N = Cudd_Regular(node);    if (cuddIsConstant(N)) {	if (node == DD_ONE(manager)) {	    return(max);	} else {	    return(0.0);	}    }    if (st_lookup(table,(char *)node,(char **)&dummy)) {	return(*dummy);    }	      Nv = cuddT(N);    Nnv = cuddE(N);    if (N != node) {	Nv = Cudd_Not(Nv);	Nnv = Cudd_Not(Nnv);    }    /* Recur on the two branches. */    min_v  = bddAnnotateMintermCount(manager,Nv,max,table) / 2.0;    if (min_v == (double)CUDD_OUT_OF_MEM)	return ((double)CUDD_OUT_OF_MEM);    min_nv = bddAnnotateMintermCount(manager,Nnv,max,table) / 2.0;    if (min_nv == (double)CUDD_OUT_OF_MEM)	return ((double)CUDD_OUT_OF_MEM);    min_N  = min_v + min_nv;    pmin = ABC_ALLOC(double,1);    if (pmin == NULL) {	manager->errorCode = CUDD_MEMORY_OUT;	return((double)CUDD_OUT_OF_MEM);    }    *pmin = min_N;    if (st_insert(table,(char *)node, (char *)pmin) == ST_OUT_OF_MEM) {	ABC_FREE(pmin);	return((double)CUDD_OUT_OF_MEM);    }        return(min_N);} /* end of bddAnnotateMintermCount */

voidst_free_table(st_table *table){    st_table_entry *ptr, *next;    int i;    for(i = 0; i < table->num_bins ; i++) {	ptr = table->bins[i];	while (ptr != NULL) {	    next = ptr->next;	    ABC_FREE(ptr);	    ptr = next;	}    }    ABC_FREE(table->bins);    ABC_FREE(table);}

/**Function*************************************************************  Synopsis    [Removes one partition.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Llb_NonlinRemovePart( Llb_Mgr_t * p, Llb_Prt_t * pPart ){    assert( p->pParts[pPart->iPart] == pPart );    p->pParts[pPart->iPart] = NULL;    Vec_IntFree( pPart->vVars );    Cudd_RecursiveDeref( p->dd, pPart->bFunc );    ABC_FREE( pPart );}

/**Function*************************************************************  Synopsis    [Performs simulation of a word-level network.]  Description [Returns vRes, a 2D array of simulation information for   the output of each bit of each object listed in vNodes. In particular,   Vec_Ptr_t * vSimObj = (Vec_Ptr_t *)Vec_PtrEntry(vRes, iObj) and  Vec_Ptr_t * vSimObjBit = (Vec_Ptr_t *)Vec_PtrEntry(vSimObj, iBit)  are arrays containing the simulation info for each object (vSimObj)   and for each output bit of this object (vSimObjBit). Alternatively,  Vec_Ptr_t * vSimObjBit = Vec_VecEntryEntry( (Vec_Vec_t *)vRes, iObj, iBit ).  The output bitwidth of an object is Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) ).  Simulation information is binary data constaining the given number (nWords)  of 64-bit machine words for the given number (nFrames) of consecutive   timeframes.  The total number of timeframes is nWords * nFrames for   each bit of each object.]                 SideEffects []  SeeAlso     []***********************************************************************/void Wlc_NtkDeleteSim( Vec_Ptr_t * p ){    word * pInfo; int i, k;    Vec_Vec_t * vVec = (Vec_Vec_t *)p;    Vec_VecForEachEntry( word *, vVec, pInfo, i, k )        ABC_FREE( pInfo );    Vec_VecFree( vVec );}

/**Function*************************************************************  Synopsis    [Stops the unit dispenser.]  Description []  SideEffects []  SeeAlso     []***********************************************************************/void reoUnitsStopDispenser( reo_man * p ){	int i;	for ( i = 0; i < p->nMemChunks; i++ )		ABC_FREE( p->pMemChunks[i] );//	printf("/nThe number of chunks used is %d, each of them %d units/n", p->nMemChunks, REO_CHUNK_SIZE );	p->nMemChunks = 0;}

/**Function*************************************************************  Synopsis    []  Description []  SideEffects []  SeeAlso     []***********************************************************************/void Mvc_ManagerFree( Mvc_Manager_t * p ){    Extra_MmFixedStop( p->pMan1 );    Extra_MmFixedStop( p->pMan2 );    Extra_MmFixedStop( p->pMan4 );    Extra_MmFixedStop( p->pManC );    ABC_FREE( p );}

/**Function********************************************************************  Synopsis    [Deletes resources associated with a DD manager.]  Description [Deletes resources associated with a DD manager and  resets the global statistical counters. (Otherwise, another manaqger  subsequently created would inherit the stats of this one.)]  SideEffects [None]  SeeAlso     [Cudd_Init]******************************************************************************/voidCudd_Quit(  DdManager * unique){    if (unique->stash != NULL) ABC_FREE(unique->stash);    cuddFreeTable(unique);} /* end of Cudd_Quit */

int main(int argc, char *argv[]){    tABC_CC cc;    tABC_Error error;    unsigned char seed[] = {1, 2, 3};    tABC_SyncKeys *pKeys = NULL;    tABC_U08Buf data;    if (argc != 8)    {        fprintf(stderr, "usage: %s <dir> <user> <pass> <wallet-name> <addr> <start> <end>/n", argv[0]);        return 1;    }    long start = atol(argv[6]);    long end = atol(argv[7]);    char *szMatchAddr = argv[5];    MAIN_CHECK(ABC_Initialize(argv[1], CA_CERT, seed, sizeof(seed), &error));    MAIN_CHECK(ABC_LoginShimGetSyncKeys(argv[2], argv[3], &pKeys, &error));    MAIN_CHECK(ABC_WalletGetBitcoinPrivateSeed(ABC_WalletID(pKeys, argv[4]), &data, &error));    for (long i = start, c = 0; i <= end; i++, ++c)    {        char *szPubAddress = NULL;        ABC_BridgeGetBitcoinPubAddress(&szPubAddress, data, (int32_t) i, NULL);        if (strncmp(szPubAddress, szMatchAddr, strlen(szMatchAddr)) == 0)        {            printf("Found %s at %ld/n", szMatchAddr, i);            ABC_FREE(szPubAddress);            break;        }        ABC_FREE(szPubAddress);        if (c == 100000)        {            printf("%ld/n", i);            c = 0;        }    }    ABC_SyncFreeKeys(pKeys);    ABC_BUF_FREE(data);    return 0;}

/**Function*************************************************************  Synopsis    [Resizes the table.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Nm_ManResize( Nm_Man_t * p ){    Nm_Entry_t ** pBinsNewI2N, ** pBinsNewN2I, * pEntry, * pEntry2, ** ppSpot;    int nBinsNew, Counter, e;    clock_t clk;clk = clock();    // get the new table size    nBinsNew = Abc_PrimeCudd( p->nGrowthFactor * p->nBins );     // allocate a new array    pBinsNewI2N = ABC_ALLOC( Nm_Entry_t *, nBinsNew );    pBinsNewN2I = ABC_ALLOC( Nm_Entry_t *, nBinsNew );    memset( pBinsNewI2N, 0, sizeof(Nm_Entry_t *) * nBinsNew );    memset( pBinsNewN2I, 0, sizeof(Nm_Entry_t *) * nBinsNew );    // rehash entries in Id->Name table    Counter = 0;    for ( e = 0; e < p->nBins; e++ )        for ( pEntry = p->pBinsI2N[e], pEntry2 = pEntry? pEntry->pNextI2N : NULL;               pEntry; pEntry = pEntry2, pEntry2 = pEntry? pEntry->pNextI2N : NULL )            {                ppSpot = pBinsNewI2N + Nm_HashNumber(pEntry->ObjId, nBinsNew);                pEntry->pNextI2N = *ppSpot;                *ppSpot = pEntry;                Counter++;            }    // rehash entries in Name->Id table    for ( e = 0; e < p->nBins; e++ )        for ( pEntry = p->pBinsN2I[e], pEntry2 = pEntry? pEntry->pNextN2I : NULL;               pEntry; pEntry = pEntry2, pEntry2 = pEntry? pEntry->pNextN2I : NULL )            {                ppSpot = pBinsNewN2I + Nm_HashString(pEntry->Name, nBinsNew);                pEntry->pNextN2I = *ppSpot;                *ppSpot = pEntry;            }    assert( Counter == p->nEntries );//    printf( "Increasing the structural table size from %6d to %6d. ", p->nBins, nBinsNew );//    ABC_PRT( "Time", clock() - clk );    // replace the table and the parameters    ABC_FREE( p->pBinsI2N );    ABC_FREE( p->pBinsN2I );    p->pBinsI2N = pBinsNewI2N;    p->pBinsN2I = pBinsNewN2I;    p->nBins = nBinsNew;//    Nm_ManProfile( p );}

/**Function*************************************************************  Synopsis    [Gets fanin node names.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Abc_NodeFreeNames( Vec_Ptr_t * vNames ){    int i;    if ( vNames == NULL )        return;    for ( i = 0; i < vNames->nSize; i++ )        ABC_FREE( vNames->pArray[i] );    Vec_PtrFree( vNames );}

/**Function*************************************************************  Synopsis    [Procedures to read/write GIA to/from MiniAIG file.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/Gia_Man_t * Gia_ManReadMiniAig( char * pFileName ){    Mini_Aig_t * p = Mini_AigLoad( pFileName );    Gia_Man_t * pGia = Gia_ManFromMiniAig( p );    ABC_FREE( pGia->pName );    pGia->pName = Extra_FileNameGeneric( pFileName );     Mini_AigStop( p );    return pGia;}

st_table *st_copy(st_table *old_table){    st_table *newEntry_table;    st_table_entry *ptr, *newEntryptr, *next, *newEntry;    int i, j, num_bins = old_table->num_bins;    newEntry_table = ABC_ALLOC(st_table, 1);    if (newEntry_table == NULL) {	return NULL;    }        *newEntry_table = *old_table;    newEntry_table->bins = ABC_ALLOC(st_table_entry *, num_bins);    if (newEntry_table->bins == NULL) {	ABC_FREE(newEntry_table);	return NULL;    }    for(i = 0; i < num_bins ; i++) {	newEntry_table->bins[i] = NULL;	ptr = old_table->bins[i];	while (ptr != NULL) {	    newEntry = ABC_ALLOC(st_table_entry, 1);	    if (newEntry == NULL) {		for (j = 0; j <= i; j++) {		    newEntryptr = newEntry_table->bins[j];		    while (newEntryptr != NULL) {			next = newEntryptr->next;			ABC_FREE(newEntryptr);			newEntryptr = next;		    }		}		ABC_FREE(newEntry_table->bins);		ABC_FREE(newEntry_table);		return NULL;	    }	    *newEntry = *ptr;	    newEntry->next = newEntry_table->bins[i];	    newEntry_table->bins[i] = newEntry;	    ptr = ptr->next;	}    }    return newEntry_table;}

/**Function********************************************************************  Synopsis    [Frees the ZDD universe.]  Description [Frees the ZDD universe.]  SideEffects [None]  SeeAlso     [cuddZddInitUniv]******************************************************************************/voidcuddZddFreeUniv(  DdManager * zdd){    if (zdd->univ) {        Cudd_RecursiveDerefZdd(zdd, zdd->univ[0]);        ABC_FREE(zdd->univ);    }} /* end of cuddZddFreeUniv */

/**Function*************************************************************  Synopsis    [This procedure transforms tech-ind Ptr into mapped Ptr.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Cba_PtrUpdateBox( Vec_Ptr_t * vBox, Vec_Ptr_t * vGatesNames ){    Mio_Gate_t * pGate;  Mio_Pin_t * pPin; int i = 1;    Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen( Abc_FrameGetGlobalFrame() );    // update gate name    char * pNameNew, * pName = (char *)Vec_PtrEntry(vBox, 0);    if ( !strcmp(pName, "Const0T") )        pNameNew = (char *)Vec_PtrEntry(vGatesNames, PTR_GATE_C0);    else if ( !strcmp(pName, "Const1T") )        pNameNew = (char *)Vec_PtrEntry(vGatesNames, PTR_GATE_C1);    else if ( !strcmp(pName, "BufT") )        pNameNew = (char *)Vec_PtrEntry(vGatesNames, PTR_GATE_BUF);    else if ( !strcmp(pName, "InvT") )        pNameNew = (char *)Vec_PtrEntry(vGatesNames, PTR_GATE_INV);    else if ( !strcmp(pName, "AndT") )        pNameNew = (char *)Vec_PtrEntry(vGatesNames, PTR_GATE_AND);    else if ( !strcmp(pName, "NandT") )        pNameNew = (char *)Vec_PtrEntry(vGatesNames, PTR_GATE_NAND);    else if ( !strcmp(pName, "OrT") )        pNameNew = (char *)Vec_PtrEntry(vGatesNames, PTR_GATE_OR);    else if ( !strcmp(pName, "NorT") )        pNameNew = (char *)Vec_PtrEntry(vGatesNames, PTR_GATE_NOR);    else if ( !strcmp(pName, "XorT") )        pNameNew = (char *)Vec_PtrEntry(vGatesNames, PTR_GATE_XOR);    else if ( !strcmp(pName, "XnorT") )        pNameNew = (char *)Vec_PtrEntry(vGatesNames, PTR_GATE_XNOR);    else // user hierarchy        return;    ABC_FREE( pName );    Vec_PtrWriteEntry( vBox, 0, Abc_UtilStrsav(pNameNew) );    // remove instance name    pName = (char *)Vec_PtrEntry(vBox, 1);    ABC_FREE( pName );    Vec_PtrWriteEntry( vBox, 1, NULL );    // update formal input names    pGate = Mio_LibraryReadGateByName( pLib, pNameNew, NULL );    Mio_GateForEachPin( pGate, pPin )    {        pName = (char *)Vec_PtrEntry( vBox, 2 * i );        ABC_FREE( pName );        pNameNew = Mio_PinReadName(pPin);        Vec_PtrWriteEntry( vBox, 2 * i++, Abc_UtilStrsav(pNameNew) );    }

void Bus_ManStop( Bus_Man_t * p ){    Vec_PtrFreeP( &p->vFanouts );    Vec_FltFreeP( &p->vWireCaps );    Vec_FltFreeP( &p->vCins );    Vec_FltFreeP( &p->vETimes );    Vec_FltFreeP( &p->vLoads );    Vec_FltFreeP( &p->vDepts );    ABC_FREE( p );}

/**Function*************************************************************  Synopsis    [Deallocates the supergate library.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Map_SuperLibFree( Map_SuperLib_t * p ){    if ( p == NULL ) return;    if ( p->pGenlib )    {        assert( p->pGenlib == Abc_FrameReadLibGen() );        Mio_LibraryDelete( p->pGenlib );        Abc_FrameSetLibGen( NULL );    }    if ( p->tTableC )        Map_SuperTableFree( p->tTableC );    if ( p->tTable )        Map_SuperTableFree( p->tTable );    Extra_MmFixedStop( p->mmSupers );    Extra_MmFixedStop( p->mmEntries );    Extra_MmFlexStop( p->mmForms );    ABC_FREE( p->ppSupers );    ABC_FREE( p );}

/**Function*************************************************************  Synopsis    []  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree ){    if ( pTree->bRel )        Cudd_RecursiveDeref( pTree->dd, pTree->bRel );    if ( pTree->bCube )        Cudd_RecursiveDeref( pTree->dd, pTree->bCube );    if ( pTree->bImage )        Cudd_RecursiveDeref( pTree->dd, pTree->bImage );    ABC_FREE( pTree );}

ABC_NAMESPACE_IMPL_START///////////////////////////////////////////////////////////////////////////                        DECLARATIONS                              //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////                     FUNCTION DEFINITIONS                         ////////////////////////////////////////////////////////////////////////////**Function*************************************************************  Synopsis    []  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Mio_LibraryDelete( Mio_Library_t * pLib ){    Mio_Gate_t * pGate, * pGate2;    if ( pLib == NULL )        return;    // free the bindings of nodes to gates from this library for all networks    Abc_FrameUnmapAllNetworks( Abc_FrameGetGlobalFrame() );    // free the library    ABC_FREE( pLib->pName );    Mio_LibraryForEachGateSafe( pLib, pGate, pGate2 )        Mio_GateDelete( pGate );    Mem_FlexStop( pLib->pMmFlex, 0 );    Vec_StrFree( pLib->vCube );    if ( pLib->tName2Gate )        st__free_table( pLib->tName2Gate );//    if ( pLib->dd )//        Cudd_Quit( pLib->dd );    ABC_FREE( pLib->ppGates0 );    ABC_FREE( pLib->ppGatesName );    ABC_FREE( pLib );}

/**Function*************************************************************  Synopsis    [Creates logic network isomorphic to the given AIG.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/Cof_Man_t * Cof_ManCreateLogicSimple( Gia_Man_t * pGia ){    Cof_Man_t * p;    Cof_Obj_t * pObjLog, * pFanLog;    Gia_Obj_t * pObj;    int * pMuxRefs;    int i, iHandle = 0;    p = ABC_CALLOC( Cof_Man_t, 1 );    p->pGia = pGia;    p->vCis = Vec_IntAlloc( Gia_ManCiNum(pGia) );    p->vCos = Vec_IntAlloc( Gia_ManCoNum(pGia) );    p->nObjData = (sizeof(Cof_Obj_t) / 4) * Gia_ManObjNum(pGia) + 4 * Gia_ManAndNum(pGia) + 2 * Gia_ManCoNum(pGia);    p->pObjData = ABC_CALLOC( int, p->nObjData );    ABC_FREE( pGia->pRefs );    Gia_ManCreateRefs( pGia );    Gia_ManForEachObj( pGia, pObj, i )    {        pObj->Value = iHandle;        pObjLog = Cof_ManObj( p, iHandle );        pObjLog->nFanins  = 0;        pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj );        pObjLog->Id       = i;        pObjLog->Value    = 0;        if ( Gia_ObjIsAnd(pObj) )        {            pFanLog = Cof_ManObj( p, Gia_ObjHandle(Gia_ObjFanin0(pObj)) );             pFanLog->Fanios[pFanLog->nFanins + pFanLog->Value++].iFan =                 pObjLog->Fanios[pObjLog->nFanins].iFan = Cof_ObjHandleDiff( pObjLog, pFanLog );            pObjLog->Fanios[pObjLog->nFanins++].fCompl = Gia_ObjFaninC0(pObj);            pFanLog = Cof_ManObj( p, Gia_ObjHandle(Gia_ObjFanin1(pObj)) );             pFanLog->Fanios[pFanLog->nFanins + pFanLog->Value++].iFan =                 pObjLog->Fanios[pObjLog->nFanins].iFan = Cof_ObjHandleDiff( pObjLog, pFanLog );            pObjLog->Fanios[pObjLog->nFanins++].fCompl = Gia_ObjFaninC1(pObj);            p->nNodes++;        }        else if ( Gia_ObjIsCo(pObj) )        {            pFanLog = Cof_ManObj( p, Gia_ObjHandle(Gia_ObjFanin0(pObj)) );             pFanLog->Fanios[pFanLog->nFanins + pFanLog->Value++].iFan =                 pObjLog->Fanios[pObjLog->nFanins].iFan = Cof_ObjHandleDiff( pObjLog, pFanLog );            pObjLog->Fanios[pObjLog->nFanins++].fCompl = Gia_ObjFaninC0(pObj);            pObjLog->fTerm = 1;            Vec_IntPush( p->vCos, iHandle );        }        else if ( Gia_ObjIsCi(pObj) )        {            pObjLog->fTerm = 1;            Vec_IntPush( p->vCis, iHandle );        }        iHandle += Cof_ObjSize( pObjLog );        p->nObjs++;    }

/**Function*************************************************************  Synopsis    [Computes and adds all single-cube divisors to storage.]  Description [This procedure should be called once when the matrix is  already contructed before the process of logic extraction begins..]                 SideEffects []  SeeAlso     []***********************************************************************/void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax ){    Fxu_Var * pVar;    Vec_Ptr_t * vSingles;    int i, k;    // set the weight limit    p->nWeightLimit = 1 - fUse0;    // iterate through columns in the matrix and collect single-cube divisors    vSingles = Vec_PtrAlloc( 10000 );    Fxu_MatrixForEachVariable( p, pVar )        Fxu_MatrixComputeSinglesOneCollect( p, pVar, vSingles );    p->nSingleTotal = Vec_PtrSize(vSingles) / 3;    // check if divisors should be filtered    if ( Vec_PtrSize(vSingles) > nSingleMax )    {        int * pWeigtCounts, nDivCount, Weight, i, c;;        assert( Vec_PtrSize(vSingles) % 3 == 0 );        // count how many divisors have the given weight        pWeigtCounts = ABC_ALLOC( int, 1000 );        memset( pWeigtCounts, 0, sizeof(int) * 1000 );        for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )        {            Weight = (int)(ABC_PTRUINT_T)Vec_PtrEntry(vSingles, i);            if ( Weight >= 999 )                pWeigtCounts[999]++;            else                pWeigtCounts[Weight]++;        }        // select the bound on the weight (above this bound, singles will be included)        nDivCount = 0;        for ( c = 999; c >= 0; c-- )        {            nDivCount += pWeigtCounts[c];            if ( nDivCount >= nSingleMax )                break;        }        ABC_FREE( pWeigtCounts );        // collect singles with the given costs        k = 0;        for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )        {            Weight = (int)(ABC_PTRUINT_T)Vec_PtrEntry(vSingles, i);            if ( Weight < c )                continue;            Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-2) );            Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-1) );            Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i) );            if ( k/3 == nSingleMax )                break;        }        Vec_PtrShrink( vSingles, k );        // adjust the weight limit        p->nWeightLimit = c;    }

/**Function*************************************************************  Synopsis    [Deletes the manager.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Fra_ClauStop( Cla_Man_t * p ){    ABC_FREE( p->pMapCsMainToCsTest );    ABC_FREE( p->pMapCsTestToCsMain );    ABC_FREE( p->pMapCsTestToNsTest );    ABC_FREE( p->pMapCsTestToNsBmc  );    Vec_IntFree( p->vSatVarsMainCs );    Vec_IntFree( p->vSatVarsTestCs );    Vec_IntFree( p->vSatVarsTestNs );    Vec_IntFree( p->vSatVarsBmcNs );    Vec_IntFree( p->vCexMain0 );    Vec_IntFree( p->vCexMain );    Vec_IntFree( p->vCexTest );    Vec_IntFree( p->vCexBase );    Vec_IntFree( p->vCexAssm );    Vec_IntFree( p->vCexBmc  );    if ( p->pSatMain ) sat_solver_delete( p->pSatMain );    if ( p->pSatTest ) sat_solver_delete( p->pSatTest );    if ( p->pSatBmc )  sat_solver_delete( p->pSatBmc );    ABC_FREE( p );}

/**Function*************************************************************  Synopsis    [Delete the partitions from the nodes.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode ){    Extra_ImagePart_t * pPart;    if ( pNode->pNode1 )        Extra_DeleteParts_rec( pNode->pNode1 );    if ( pNode->pNode2 )        Extra_DeleteParts_rec( pNode->pNode2 );    pPart = pNode->pPart;    Cudd_RecursiveDeref( pNode->dd, pPart->bFunc );    Cudd_RecursiveDeref( pNode->dd, pPart->bSupp );    ABC_FREE( pNode->pPart );}

/**Function********************************************************************  Synopsis [This function prepares an array of variables which have not been  encountered so far when traversing the procedure cuddSplitSetRecur.]  Description [This function prepares an array of variables which have not been  encountered so far when traversing the procedure cuddSplitSetRecur. This  array is then used to extract the required number of minterms from a constant  1. The algorithm guarantees that the size of BDD will be utmost /log(n).]  SideEffects [None]******************************************************************************/static DdNode *selectMintermsFromUniverse(  DdManager * manager,  int * varSeen,  double  n){    int numVars;    int i, size, j;     DdNode *one, *zero, *result;    DdNode **vars;    numVars = 0;    size = manager->size;    one = DD_ONE(manager);    zero = Cudd_Not(one);    /* Count the number of variables not encountered so far in procedure    ** cuddSplitSetRecur.    */    for (i = size-1; i >= 0; i--) {	if(varSeen[i] == 0)	    numVars++;    }    vars = ABC_ALLOC(DdNode *, numVars);    if (!vars) {	manager->errorCode = CUDD_MEMORY_OUT;	return(NULL);    }    j = 0;    for (i = size-1; i >= 0; i--) {	if(varSeen[i] == 0) {	    vars[j] = cuddUniqueInter(manager,manager->perm[i],one,zero);	    cuddRef(vars[j]);	    j++;	}    }    /* Compute a function which has n minterms and depends on at most    ** numVars variables.    */    result = mintermsFromUniverse(manager,vars,numVars,n, 0);    if (result) 	cuddRef(result);    for (i = 0; i < numVars; i++)	Cudd_RecursiveDeref(manager,vars[i]);    ABC_FREE(vars);    return(result);} /* end of selectMintermsFromUniverse */

/**Function********************************************************************  Synopsis    [Shuts down a level queue.]  Description [Shuts down a level queue and releases all the  associated memory.]  SideEffects [None]  SeeAlso     [cuddLevelQueueInit]******************************************************************************/voidcuddLevelQueueQuit(  DdLevelQueue * queue){    DdQueueItem *item;    while (queue->freelist != NULL) {        item = queue->freelist;        queue->freelist = item->next;        ABC_FREE(item);    }    while (queue->first != NULL) {        item = (DdQueueItem *) queue->first;        queue->first = item->next;        ABC_FREE(item);    }    ABC_FREE(queue->buckets);    ABC_FREE(queue->last);    ABC_FREE(queue);    return;} /* end of cuddLevelQueueQuit */

/**Function*************************************************************  Synopsis    []  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Abc_FrameDeallocate( Abc_Frame_t * p ){    extern void Rwt_ManGlobalStop();    extern void undefine_cube_size();//    extern void Ivy_TruthManStop();//    Abc_HManStop();//    undefine_cube_size();    Rwt_ManGlobalStop();//    Ivy_TruthManStop();    if ( p->pLibVer ) Abc_LibFree( (Abc_Lib_t *)p->pLibVer, NULL );    if ( p->pManDec ) Dec_ManStop( (Dec_Man_t *)p->pManDec );    if ( p->dd )      Extra_StopManager( p->dd );    if ( p->vStore )  Vec_PtrFree( p->vStore );    if ( p->pSave1 )  Aig_ManStop( (Aig_Man_t *)p->pSave1 );    if ( p->pSave2 )  Aig_ManStop( (Aig_Man_t *)p->pSave2 );    if ( p->pSave3 )  Aig_ManStop( (Aig_Man_t *)p->pSave3 );    if ( p->pSave4 )  Aig_ManStop( (Aig_Man_t *)p->pSave4 );    Abc_FrameDeleteAllNetworks( p );    ABC_FREE( p->pCex );    ABC_FREE( p );    s_GlobalFrame = NULL;}

/**Function*************************************************************  Synopsis    []  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Ssc_ManStop( Ssc_Man_t * p ){    Vec_IntFreeP( &p->vFront );    Vec_IntFreeP( &p->vFanins );    Vec_IntFreeP( &p->vPattern );    Vec_IntFreeP( &p->vDisPairs );    Vec_IntFreeP( &p->vPivot );    Vec_IntFreeP( &p->vId2Var );    Vec_IntFreeP( &p->vVar2Id );    if ( p->pSat ) sat_solver_delete( p->pSat );    Gia_ManStopP( &p->pFraig );    ABC_FREE( p );}

/**Function*************************************************************  Synopsis    []  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Cov_ManFree( Cov_Man_t * p ){    Vec_Int_t * vSupp;    int i;    for ( i = 0; i < p->vObjStrs->nSize; i++ )    {        vSupp = ((Cov_Obj_t *)p->vObjStrs->pArray[i])->vSupp;        if ( vSupp ) Vec_IntFree( vSupp );    }    Min_ManFree( p->pManMin );    Vec_PtrFree( p->vObjStrs );    Vec_IntFree( p->vFanCounts );    Vec_IntFree( p->vTriv0 );    Vec_IntFree( p->vTriv1 );    Vec_IntFree( p->vComTo0 );    Vec_IntFree( p->vComTo1 );    Vec_IntFree( p->vPairs0 );    Vec_IntFree( p->vPairs1 );    ABC_FREE( p->pMemory );    ABC_FREE( p );}

/**Function*************************************************************  Synopsis    [Stops the simulation manager.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Sim_ManStop( Sim_Man_t * p ){    Sim_ManPrintStats( p );    if ( p->vSim0 )        Sim_UtilInfoFree( p->vSim0 );           if ( p->vSim1 )        Sim_UtilInfoFree( p->vSim1 );           if ( p->vSuppStr )     Sim_UtilInfoFree( p->vSuppStr );    //    if ( p->vSuppFun )     Sim_UtilInfoFree( p->vSuppFun );        if ( p->vSuppTargs )   Vec_VecFree( p->vSuppTargs );    if ( p->pMmPat )       Extra_MmFixedStop( p->pMmPat );    if ( p->vFifo )        Vec_PtrFree( p->vFifo );    if ( p->vDiffs )       Vec_IntFree( p->vDiffs );    ABC_FREE( p );}