summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satTruth.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bsat/satTruth.c')
-rw-r--r--src/sat/bsat/satTruth.c315
1 files changed, 315 insertions, 0 deletions
diff --git a/src/sat/bsat/satTruth.c b/src/sat/bsat/satTruth.c
new file mode 100644
index 00000000..7d69f558
--- /dev/null
+++ b/src/sat/bsat/satTruth.c
@@ -0,0 +1,315 @@
+/**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 "vecRec.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_Rec_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_RecEntryP(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_RecEntryNum(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_RecEntryNum(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_RecAppend( p->pMem, 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] =
+ {
+ 0xAAAAAAAAAAAAAAAA,
+ 0xCCCCCCCCCCCCCCCC,
+ 0xF0F0F0F0F0F0F0F0,
+ 0xFF00FF00FF00FF00,
+ 0xFFFF0000FFFF0000,
+ 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_RecAlloc();
+ // 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_RecEntryNum(p->pMem) );
+ Vec_RecFree( 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;
+ assert( Vec_RecChunk(h) );
+ return Tru_ManReadOne( p, h )->pTruth;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns stored truth table]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Tru_ManHandleMax( Tru_Man_t * p )
+{
+ return p->pMem->hCurrent;
+}
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 18:19:21 +0000