abc/src/base/abci/abcExact.c
// pArrTimeProfile is normalized
// returns 1 if and only if a new TimesEntry has been created
pArrTimeProfile is normalized
returns 1 if and only if a new TimesEntry has been created
pArrTimeProfile is normalized returns 1 if and only if a new TimesEntry has been created
int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char * pSol, int fResLimit )
{
    int key, fAdded;
    Ses_TruthEntry_t * pTEntry;
    Ses_TimesEntry_t * pTiEntry;
    if ( pSol )
        Abc_ExactNormalizeArrivalTimesForNetwork( nVars, pArrTimeProfile, pSol );
    key = Ses_StoreTableHash( pTruth, nVars );
    pTEntry = pStore->pEntries[key];
    while ( pTEntry )
    {
        if ( Ses_StoreTruthEqual( pTEntry, pTruth, nVars ) )
            break;
        else
            pTEntry = pTEntry->next;
    }
    if ( !pTEntry )
    {
        pTEntry = ABC_CALLOC( Ses_TruthEntry_t, 1 );
        Ses_StoreTruthCopy( pTEntry, pTruth, nVars );
        pTEntry->next = pStore->pEntries[key];
        pStore->pEntries[key] = pTEntry;
    }
    pTiEntry = pTEntry->head;
    while ( pTiEntry )
    {
        if ( Ses_StoreTimesEqual( pArrTimeProfile, pTiEntry->pArrTimeProfile, nVars ) )
            break;
        else
            pTiEntry = pTiEntry->next;
    }
    if ( !pTiEntry )
    {
        pTiEntry = ABC_CALLOC( Ses_TimesEntry_t, 1 );
        Ses_StoreTimesCopy( pTiEntry->pArrTimeProfile, pArrTimeProfile, nVars );
        pTiEntry->pNetwork = pSol;
        pTiEntry->fResLimit = fResLimit;
        pTiEntry->next = pTEntry->head;
        pTEntry->head = pTiEntry;
        fAdded = 1;
        pStore->nEntriesCount++;
        if ( pSol )
            pStore->nValidEntriesCount++;
    }
    else
    {
        fAdded = 0;
    }
    if ( pSol )
    {
        if ( fResLimit )
        {
            pStore->nSynthesizedRL++;
            pStore->pSynthesizedRL[nVars]++;
        }
        else
        {
            pStore->nSynthesizedImp++;
            pStore->pSynthesizedImp[nVars]++;
        }
    }
    else
    {
        if ( fResLimit )
        {
            pStore->nUnsynthesizedRL++;
            pStore->pUnsynthesizedRL[nVars]++;
        }
        else
        {
            pStore->nUnsynthesizedImp++;
            pStore->pUnsynthesizedImp[nVars]++;
        }
    }
    if ( fAdded && pStore->szDBName )
        Ses_StoreWrite( pStore, pStore->szDBName, 1, 0, 0, 0 );
    return fAdded;
}
int Ses_StoreAddEntry ( Ses_Store_t * pStore , word * pTruth , int nVars , int * pArrTimeProfile , char * pSol , int fResLimit ) { int key , fAdded ; Ses_TruthEntry_t * pTEntry ; Ses_TimesEntry_t * pTiEntry ; if ( pSol ) Abc_ExactNormalizeArrivalTimesForNetwork ( nVars , pArrTimeProfile , pSol ) ; key = Ses_StoreTableHash ( pTruth , nVars ) ; pTEntry = pStore -> pEntries [ key ] ; while ( pTEntry ) { if ( Ses_StoreTruthEqual ( pTEntry , pTruth , nVars ) ) break ; else pTEntry = pTEntry -> next ; } if ( ! pTEntry ) { pTEntry = ABC_CALLOC ( Ses_TruthEntry_t , 1 ) ; Ses_StoreTruthCopy ( pTEntry , pTruth , nVars ) ; pTEntry -> next = pStore -> pEntries [ key ] ; pStore -> pEntries [ key ] = pTEntry ; } pTiEntry = pTEntry -> head ; while ( pTiEntry ) { if ( Ses_StoreTimesEqual ( pArrTimeProfile , pTiEntry -> pArrTimeProfile , nVars ) ) break ; else pTiEntry = pTiEntry -> next ; } if ( ! pTiEntry ) { pTiEntry = ABC_CALLOC ( Ses_TimesEntry_t , 1 ) ; Ses_StoreTimesCopy ( pTiEntry -> pArrTimeProfile , pArrTimeProfile , nVars ) ; pTiEntry -> pNetwork = pSol ; pTiEntry -> fResLimit = fResLimit ; pTiEntry -> next = pTEntry -> head ; pTEntry -> head = pTiEntry ; fAdded = 1 ; pStore -> nEntriesCount ++ ; if ( pSol ) pStore -> nValidEntriesCount ++ ; } else { fAdded = 0 ; } if ( pSol ) { if ( fResLimit ) { pStore -> nSynthesizedRL ++ ; pStore -> pSynthesizedRL [ nVars ] ++ ; } else { pStore -> nSynthesizedImp ++ ; pStore -> pSynthesizedImp [ nVars ] ++ ; } } else { if ( fResLimit ) { pStore -> nUnsynthesizedRL ++ ; pStore -> pUnsynthesizedRL [ nVars ] ++ ; } else { pStore -> nUnsynthesizedImp ++ ; pStore -> pUnsynthesizedImp [ nVars ] ++ ; } } if ( fAdded && pStore -> szDBName ) Ses_StoreWrite ( pStore , pStore -> szDBName , 1 , 0 , 0 , 0 ) ; return fAdded ; }
pArrTimeProfile is normalized
returns 1 if and only if a new TimesEntry has been created
pArrTimeProfile is normalized returns 1 if and only if a new TimesEntry has been created
/* does truth table already exist? */ /* entry does not yet exist, so create new one and enqueue */ /* does arrival time already exist? */ /* entry does not yet exist, so create new one and enqueue */ /* item has been added */ //assert( 0 ); /* item was already present */ /* statistics */