| /**CFile**************************************************************** |
| |
| FileName [satTruth.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [SAT solver.] |
| |
| Synopsis [Truth table computation package.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: satTruth.c,v 1.4 2005/09/16 22:55:03 casem Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "satTruth.h" |
| #include "misc/vec/vecSet.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| struct Tru_Man_t_ |
| { |
| int nVars; // the number of variables |
| int nWords; // the number of words in the truth table |
| int nEntrySize; // the size of one entry in 'int' |
| int nTableSize; // hash table size |
| int * pTable; // hash table |
| Vec_Set_t * pMem; // memory for truth tables |
| word * pZero; // temporary truth table |
| int hIthVars[16]; // variable handles |
| int nTableLookups; |
| }; |
| |
| typedef struct Tru_One_t_ Tru_One_t; // 16 bytes minimum |
| struct Tru_One_t_ |
| { |
| int Handle; // support |
| int Next; // next one in the table |
| word pTruth[0]; // truth table |
| }; |
| |
| static inline Tru_One_t * Tru_ManReadOne( Tru_Man_t * p, int h ) { return h ? (Tru_One_t *)Vec_SetEntry(p->pMem, h) : NULL; } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the hash key.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline unsigned Tru_ManHash( word * pTruth, int nWords, int nBins, int * pPrimes ) |
| { |
| int i; |
| unsigned uHash = 0; |
| for ( i = 0; i < nWords; i++ ) |
| uHash ^= pTruth[i] * pPrimes[i & 0x7]; |
| return uHash % nBins; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the given record.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int * Tru_ManLookup( Tru_Man_t * p, word * pTruth ) |
| { |
| static int s_Primes[10] = { 1291, 1699, 2357, 4177, 5147, 5647, 6343, 7103, 7873, 8147 }; |
| Tru_One_t * pEntry; |
| int * pSpot; |
| assert( (pTruth[0] & 1) == 0 ); |
| pSpot = p->pTable + Tru_ManHash( pTruth, p->nWords, p->nTableSize, s_Primes ); |
| for ( pEntry = Tru_ManReadOne(p, *pSpot); pEntry; pSpot = &pEntry->Next, pEntry = Tru_ManReadOne(p, *pSpot) ) |
| if ( Tru_ManEqual(pEntry->pTruth, pTruth, p->nWords) ) |
| return pSpot; |
| return pSpot; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the given record.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Tru_ManResize( Tru_Man_t * p ) |
| { |
| Tru_One_t * pThis; |
| int * pTableOld, * pSpot; |
| int nTableSizeOld, iNext, Counter, i; |
| assert( p->pTable != NULL ); |
| // replace the table |
| pTableOld = p->pTable; |
| nTableSizeOld = p->nTableSize; |
| p->nTableSize = 2 * p->nTableSize + 1; |
| p->pTable = ABC_CALLOC( int, p->nTableSize ); |
| // rehash the entries from the old table |
| Counter = 0; |
| for ( i = 0; i < nTableSizeOld; i++ ) |
| for ( pThis = Tru_ManReadOne(p, pTableOld[i]), |
| iNext = (pThis? pThis->Next : 0); |
| pThis; pThis = Tru_ManReadOne(p, iNext), |
| iNext = (pThis? pThis->Next : 0) ) |
| { |
| assert( pThis->Handle ); |
| pThis->Next = 0; |
| pSpot = Tru_ManLookup( p, pThis->pTruth ); |
| assert( *pSpot == 0 ); // should not be there |
| *pSpot = pThis->Handle; |
| Counter++; |
| } |
| assert( Counter == Vec_SetEntryNum(p->pMem) ); |
| ABC_FREE( pTableOld ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Adds entry to the hash table.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Tru_ManInsert( Tru_Man_t * p, word * pTruth ) |
| { |
| int fCompl, * pSpot; |
| if ( Tru_ManEqual0(pTruth, p->nWords) ) |
| return 0; |
| if ( Tru_ManEqual1(pTruth, p->nWords) ) |
| return 1; |
| p->nTableLookups++; |
| if ( Vec_SetEntryNum(p->pMem) > 2 * p->nTableSize ) |
| Tru_ManResize( p ); |
| fCompl = pTruth[0] & 1; |
| if ( fCompl ) |
| Tru_ManNot( pTruth, p->nWords ); |
| pSpot = Tru_ManLookup( p, pTruth ); |
| if ( *pSpot == 0 ) |
| { |
| Tru_One_t * pEntry; |
| *pSpot = Vec_SetAppend( p->pMem, NULL, p->nEntrySize ); |
| assert( (*pSpot & 1) == 0 ); |
| pEntry = Tru_ManReadOne( p, *pSpot ); |
| Tru_ManCopy( pEntry->pTruth, pTruth, p->nWords ); |
| pEntry->Handle = *pSpot; |
| pEntry->Next = 0; |
| } |
| if ( fCompl ) |
| Tru_ManNot( pTruth, p->nWords ); |
| return *pSpot ^ fCompl; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Start the truth table logging.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Tru_Man_t * Tru_ManAlloc( int nVars ) |
| { |
| word Masks[6] = |
| { |
| ABC_CONST(0xAAAAAAAAAAAAAAAA), |
| ABC_CONST(0xCCCCCCCCCCCCCCCC), |
| ABC_CONST(0xF0F0F0F0F0F0F0F0), |
| ABC_CONST(0xFF00FF00FF00FF00), |
| ABC_CONST(0xFFFF0000FFFF0000), |
| ABC_CONST(0xFFFFFFFF00000000) |
| }; |
| Tru_Man_t * p; |
| int i, w; |
| assert( nVars > 0 && nVars <= 16 ); |
| p = ABC_CALLOC( Tru_Man_t, 1 ); |
| p->nVars = nVars; |
| p->nWords = (nVars < 6) ? 1 : (1 << (nVars-6)); |
| p->nEntrySize = (sizeof(Tru_One_t) + p->nWords * sizeof(word))/sizeof(int); |
| p->nTableSize = 8147; |
| p->pTable = ABC_CALLOC( int, p->nTableSize ); |
| p->pMem = Vec_SetAlloc( 16 ); |
| // initialize truth tables |
| p->pZero = ABC_ALLOC( word, p->nWords ); |
| for ( i = 0; i < nVars; i++ ) |
| { |
| for ( w = 0; w < p->nWords; w++ ) |
| if ( i < 6 ) |
| p->pZero[w] = Masks[i]; |
| else if ( w & (1 << (i-6)) ) |
| p->pZero[w] = ~(word)0; |
| else |
| p->pZero[w] = 0; |
| p->hIthVars[i] = Tru_ManInsert( p, p->pZero ); |
| assert( !i || p->hIthVars[i] > p->hIthVars[i-1] ); |
| } |
| Tru_ManClear( p->pZero, p->nWords ); |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Stop the truth table logging.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Tru_ManFree( Tru_Man_t * p ) |
| { |
| printf( "Lookups = %d. Entries = %d.\n", p->nTableLookups, Vec_SetEntryNum(p->pMem) ); |
| Vec_SetFree( p->pMem ); |
| ABC_FREE( p->pZero ); |
| ABC_FREE( p->pTable ); |
| ABC_FREE( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns elementary variable.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| word * Tru_ManVar( Tru_Man_t * p, int v ) |
| { |
| assert( v >= 0 && v < p->nVars ); |
| return Tru_ManReadOne( p, p->hIthVars[v] )->pTruth; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns stored truth table] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| word * Tru_ManFunc( Tru_Man_t * p, int h ) |
| { |
| assert( (h & 1) == 0 ); |
| if ( h == 0 ) |
| return p->pZero; |
| return Tru_ManReadOne( p, h )->pTruth; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
