satTruth.c File Reference

#include "satTruth.h"
#include "misc/vec/vecSet.h"

Include dependency graph for satTruth.c:

Go to the source code of this file.

Classes
struct	Tru_Man_t_
	DECLARATIONS ///. More...
struct	Tru_One_t_

Typedefs
typedef struct Tru_One_t_	Tru_One_t

Functions
int *	Tru_ManLookup (Tru_Man_t *p, word *pTruth)
void	Tru_ManResize (Tru_Man_t *p)
int	Tru_ManInsert (Tru_Man_t *p, word *pTruth)
Tru_Man_t *	Tru_ManAlloc (int nVars)
	FUNCTION DECLARATIONS ///.
void	Tru_ManFree (Tru_Man_t *p)
word *	Tru_ManVar (Tru_Man_t *p, int v)
word *	Tru_ManFunc (Tru_Man_t *p, int h)

Typedef Documentation

Tru_One_t

typedef struct Tru_One_t_ Tru_One_t

Definition at line 48 of file satTruth.c.

Function Documentation

Tru_ManAlloc()

Tru_Man_t * Tru_ManAlloc

(

int

nVars

)

FUNCTION DECLARATIONS ///.

Function*************************************************************

Synopsis [Start the truth table logging.]

Description []

SideEffects []

SeeAlso []

Definition at line 198 of file satTruth.c.

{
    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;
}

Here is the call graph for this function:

Tru_ManFree()

void Tru_ManFree

(

Tru_Man_t *

p

)

Function*************************************************************

Synopsis [Stop the truth table logging.]

Description []

SideEffects []

SeeAlso []

Definition at line 248 of file satTruth.c.

{
    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 );
}

Tru_ManFunc()

word * Tru_ManFunc	(	Tru_Man_t *	p,
		int	h )

Function*************************************************************

Synopsis [Returns stored truth table]

Description []

SideEffects []

SeeAlso []

Definition at line 285 of file satTruth.c.

{
    assert( (h & 1) == 0 );
    if ( h == 0 )
        return p->pZero;
    return Tru_ManReadOne( p, h )->pTruth;
}

Tru_ManInsert()

int Tru_ManInsert	(	Tru_Man_t *	p,
		word *	pTruth )

Function*************************************************************

Synopsis [Adds entry to the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 158 of file satTruth.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Tru_ManLookup()

int * Tru_ManLookup	(	Tru_Man_t *	p,
		word *	pTruth )

Function*************************************************************

Synopsis [Returns the given record.]

Description []

SideEffects []

SeeAlso []

Definition at line 93 of file satTruth.c.

{
    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;
}

Here is the caller graph for this function:

Tru_ManResize()

void Tru_ManResize

(

Tru_Man_t *

p

)

Function*************************************************************

Synopsis [Returns the given record.]

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file satTruth.c.

{
    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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Tru_ManVar()

word * Tru_ManVar	(	Tru_Man_t *	p,
		int	v )

Function*************************************************************

Synopsis [Returns elementary variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 268 of file satTruth.c.

{
    assert( v >= 0 && v < p->nVars );
    return Tru_ManReadOne( p, p->hIthVars[v] )->pTruth;
}