diff options
Diffstat (limited to 'src/sat/bsat/satTruth.h')
| -rw-r--r-- | src/sat/bsat/satTruth.h | 89 |
1 files changed, 89 insertions, 0 deletions
diff --git a/src/sat/bsat/satTruth.h b/src/sat/bsat/satTruth.h new file mode 100644 index 00000000..e07518b0 --- /dev/null +++ b/src/sat/bsat/satTruth.h @@ -0,0 +1,89 @@ +/**CFile**************************************************************** + + FileName [satTruth.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT solver.] + + Synopsis [Truth table computation package.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + 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 $] + +***********************************************************************/ + +#ifndef __SAT_TRUTH_H__ +#define __SAT_TRUTH_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include "abc_global.h" + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Tru_Man_t_ Tru_Man_t; + +//////////////////////////////////////////////////////////////////////// +/// GLOBAL VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Tru_ManEqual( word * pOut, word * pIn, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if(pOut[w]!=pIn[w]) return 0; return 1; } +static inline int Tru_ManEqual0( word * pOut, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if(pOut[w]!=0) return 0; return 1; } +static inline int Tru_ManEqual1( word * pOut, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if(pOut[w]!=~(word)0)return 0; return 1; } +static inline word * Tru_ManCopy( word * pOut, word * pIn, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] = pIn[w]; return pOut; } +static inline word * Tru_ManClear( word * pOut, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] = 0; return pOut; } +static inline word * Tru_ManFill( word * pOut, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] = ~(word)0; return pOut; } +static inline word * Tru_ManNot( word * pOut, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] = ~pOut[w]; return pOut; } +static inline word * Tru_ManAnd( word * pOut, word * pIn, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] &= pIn[w]; return pOut; } +static inline word * Tru_ManOr( word * pOut, word * pIn, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] |= pIn[w]; return pOut; } +static inline word * Tru_ManCopyNot( word * pOut, word * pIn, int nWords ){ int w; for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn[w]; return pOut; } +static inline word * Tru_ManAndNot( word * pOut, word * pIn, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] &= ~pIn[w]; return pOut; } +static inline word * Tru_ManOrNot( word * pOut, word * pIn, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] |= ~pIn[w]; return pOut; } +static inline word * Tru_ManCopyNotCond( word * pOut, word * pIn, int nWords, int fCompl ){ return fCompl ? Tru_ManCopyNot(pOut, pIn, nWords) : Tru_ManCopy(pOut, pIn, nWords); } +static inline word * Tru_ManAndNotCond( word * pOut, word * pIn, int nWords, int fCompl ) { return fCompl ? Tru_ManAndNot(pOut, pIn, nWords) : Tru_ManAnd(pOut, pIn, nWords); } +static inline word * Tru_ManOrNotCond( word * pOut, word * pIn, int nWords, int fCompl ) { return fCompl ? Tru_ManOrNot(pOut, pIn, nWords) : Tru_ManOr(pOut, pIn, nWords); } + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern Tru_Man_t * Tru_ManAlloc( int nVars ); +extern void Tru_ManFree( Tru_Man_t * p ); +extern word * Tru_ManVar( Tru_Man_t * p, int v ); +extern word * Tru_ManFunc( Tru_Man_t * p, int h ); +extern int Tru_ManInsert( Tru_Man_t * p, word * pTruth ); +extern int Tru_ManHandleMax( Tru_Man_t * p ); + +ABC_NAMESPACE_HEADER_END + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + |