/**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