satTruth.h File Reference

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

Go to the source code of this file.

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Tru_Man_t_	Tru_Man_t
	INCLUDES ///. More...

Functions
static int	Tru_ManEqual (word *pOut, word *pIn, int nWords)
	GLOBAL VARIABLES ///. More...
static int	Tru_ManEqual0 (word *pOut, int nWords)
static int	Tru_ManEqual1 (word *pOut, int nWords)
static word *	Tru_ManCopy (word *pOut, word *pIn, int nWords)
static word *	Tru_ManClear (word *pOut, int nWords)
static word *	Tru_ManFill (word *pOut, int nWords)
static word *	Tru_ManNot (word *pOut, int nWords)
static word *	Tru_ManAnd (word *pOut, word *pIn, int nWords)
static word *	Tru_ManOr (word *pOut, word *pIn, int nWords)
static word *	Tru_ManCopyNot (word *pOut, word *pIn, int nWords)
static word *	Tru_ManAndNot (word *pOut, word *pIn, int nWords)
static word *	Tru_ManOrNot (word *pOut, word *pIn, int nWords)
static word *	Tru_ManCopyNotCond (word *pOut, word *pIn, int nWords, int fCompl)
static word *	Tru_ManAndNotCond (word *pOut, word *pIn, int nWords, int fCompl)
static word *	Tru_ManOrNotCond (word *pOut, word *pIn, int nWords, int fCompl)
Tru_Man_t *	Tru_ManAlloc (int nVars)
	FUNCTION DECLARATIONS ///. More...
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

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

static word* Tru_ManAnd ( word *  pOut, word *  pIn, int  nWords  )

inlinestatic

Definition at line 61 of file satTruth.h.

{ int w; for ( w = 0; w < nWords; w++ ) pOut[w] &=  pIn[w];  return pOut;        }

static word* Tru_ManAndNot ( word *  pOut, word *  pIn, int  nWords  )

inlinestatic

Definition at line 64 of file satTruth.h.

{ int w; for ( w = 0; w < nWords; w++ ) pOut[w] &= ~pIn[w];  return pOut;        }

static word* Tru_ManAndNotCond ( word *  pOut, word *  pIn, int  nWords, int  fCompl  )

inlinestatic

Definition at line 67 of file satTruth.h.

{ return fCompl ? Tru_ManAndNot(pOut, pIn, nWords)  : Tru_ManAnd(pOut, pIn, nWords);  }

static word* Tru_ManClear ( word *  pOut, int  nWords  )

inlinestatic

Definition at line 58 of file satTruth.h.

{ int w; for ( w = 0; w < nWords; w++ ) pOut[w] = 0;         return pOut;        }

static word* Tru_ManCopy ( word *  pOut, word *  pIn, int  nWords  )

inlinestatic

Definition at line 57 of file satTruth.h.

{ int w; for ( w = 0; w < nWords; w++ ) pOut[w] =   pIn[w];  return pOut;        }

static word* Tru_ManCopyNot ( word *  pOut, word *  pIn, int  nWords  )

inlinestatic

Definition at line 63 of file satTruth.h.

{ int w; for ( w = 0; w < nWords; w++ ) pOut[w] =  ~pIn[w];  return pOut;        }

static word* Tru_ManCopyNotCond ( word *  pOut, word *  pIn, int  nWords, int  fCompl  )

inlinestatic

Definition at line 66 of file satTruth.h.

{ return fCompl ? Tru_ManCopyNot(pOut, pIn, nWords) : Tru_ManCopy(pOut, pIn, nWords); }

static int Tru_ManEqual ( word *  pOut, word *  pIn, int  nWords  )

inlinestatic

GLOBAL VARIABLES ///.

MACRO DEFINITIONS ///

Definition at line 54 of file satTruth.h.

{ int w; for ( w = 0; w < nWords; w++ ) if(pOut[w]!=pIn[w])  return 0; return 1; }

static int Tru_ManEqual0 ( word *  pOut, int  nWords  )

inlinestatic

Definition at line 55 of file satTruth.h.

{ int w; for ( w = 0; w < nWords; w++ ) if(pOut[w]!=0)       return 0; return 1; }

static int Tru_ManEqual1 ( word *  pOut, int  nWords  )

inlinestatic

Definition at line 56 of file satTruth.h.

{ int w; for ( w = 0; w < nWords; w++ ) if(pOut[w]!=~(word)0)return 0; return 1; }

static word* Tru_ManFill ( word *  pOut, int  nWords  )

inlinestatic

Definition at line 59 of file satTruth.h.

{ int w; for ( w = 0; w < nWords; w++ ) pOut[w] = ~(word)0;  return pOut;        }

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

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

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

static word* Tru_ManNot ( word *  pOut, int  nWords  )

inlinestatic

Definition at line 60 of file satTruth.h.

{ int w; for ( w = 0; w < nWords; w++ ) pOut[w] = ~pOut[w];  return pOut;        }

static word* Tru_ManOr ( word *  pOut, word *  pIn, int  nWords  )

inlinestatic

Definition at line 62 of file satTruth.h.

{ int w; for ( w = 0; w < nWords; w++ ) pOut[w] |=  pIn[w];  return pOut;        }

static word* Tru_ManOrNot ( word *  pOut, word *  pIn, int  nWords  )

inlinestatic

Definition at line 65 of file satTruth.h.

{ int w; for ( w = 0; w < nWords; w++ ) pOut[w] |= ~pIn[w];  return pOut;        }

static word* Tru_ManOrNotCond ( word *  pOut, word *  pIn, int  nWords, int  fCompl  )

inlinestatic

Definition at line 68 of file satTruth.h.

{ return fCompl ? Tru_ManOrNot(pOut, pIn, nWords)   : Tru_ManOr(pOut, pIn, nWords);   }

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