satTruth.h

Go to the documentation of this file.

 
#ifndef ABC__sat__bsat__satTruth_h
#define ABC__sat__bsat__satTruth_h

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


 
typedef struct Tru_Man_t_ Tru_Man_t;


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

 
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