satTruth.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/util/abc_global.h"

Include dependency graph for satTruth.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Tru_Man_t_	Tru_Man_t
	INCLUDES ///.

Functions
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)
int	Tru_ManInsert (Tru_Man_t *p, word *pTruth)

Typedef Documentation

Tru_Man_t

typedef typedefABC_NAMESPACE_HEADER_START struct Tru_Man_t_ Tru_Man_t

INCLUDES ///.

CFile****************************************************************

FileName [satTruth.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT solver.]

Synopsis [Truth table computation package.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 1, 2004.]

Revision [

Id

satTruth.h,v 1.0 2004/01/01 1:00:00 alanmi Exp

] PARAMETERS /// STRUCTURE DEFINITIONS ///

Definition at line 44 of file satTruth.h.

Function Documentation

Tru_ManAlloc()

Tru_Man_t * Tru_ManAlloc ( int nVars )

extern

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 )

extern

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 )

extern

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 )

extern

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_ManVar()

word * Tru_ManVar ( Tru_Man_t * p, int v )

extern

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