diff options
Diffstat (limited to 'src/misc/extra/extra.h')
-rw-r--r-- | src/misc/extra/extra.h | 364 |
1 files changed, 333 insertions, 31 deletions
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index f36b113f..314257a2 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -29,6 +29,10 @@ #ifndef __EXTRA_H__ #define __EXTRA_H__ +#ifdef __cplusplus +extern "C" { +#endif + #ifdef _WIN32 #define inline __inline // compatible with MS VS 6.0 #endif @@ -37,9 +41,15 @@ /* Nested includes */ /*---------------------------------------------------------------------------*/ +// this include should be the first one in the list +// it is used to catch memory leaks on Windows +#include "leaks.h" + +#include <stdio.h> +#include <stdlib.h> #include <string.h> +#include <assert.h> #include <time.h> -#include "util.h" #include "st.h" #include "cuddInt.h" @@ -63,6 +73,15 @@ /* Macro declarations */ /*---------------------------------------------------------------------------*/ +typedef unsigned char uint8; +typedef unsigned short uint16; +typedef unsigned int uint32; +#ifdef WIN32 +typedef unsigned __int64 uint64; +#else +typedef unsigned long long uint64; +#endif + /* constants of the manager */ #define b0 Cudd_Not((dd)->one) #define b1 (dd)->one @@ -91,13 +110,59 @@ #ifndef PRT #define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)) +#define PRTn(a,t) printf("%s = ", (a)); printf("%6.2f sec ", (float)(t)/(float)(CLOCKS_PER_SEC)) +#endif + +#ifndef PRTP +#define PRTP(a,t,T) printf("%s = ", (a)); printf("%6.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0) #endif /*===========================================================================*/ /* Various Utilities */ /*===========================================================================*/ -/*=== extraUtilBdd.c ========================================================*/ +/*=== extraBddAuto.c ========================================================*/ + +extern DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc ); +extern DdNode * Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ); +extern DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ); +extern DdNode * Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc ); +extern DdNode * extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc ); +extern DdNode * Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc ); +extern DdNode * extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc ); + +extern DdNode * Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace ); +extern DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bSpace ); + +extern DdNode * Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace ); +extern DdNode * Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace ); +extern DdNode * extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace ); +extern DdNode * Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace ); +extern DdNode * extraBddSpaceEquationsPos( DdManager * dd, DdNode * bSpace ); + +extern DdNode * Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ); +extern DdNode * extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ); +extern DdNode * Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ); +extern DdNode * extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ); + +extern DdNode * Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars ); +extern DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations ); + +/*=== extraBddCas.c =============================================================*/ + +/* performs the binary encoding of the set of function using the given vars */ +extern DdNode * Extra_bddEncodingBinary( DdManager * dd, DdNode ** pbFuncs, int nFuncs, DdNode ** pbVars, int nVars ); +/* solves the column encoding problem using a sophisticated method */ +extern DdNode * Extra_bddEncodingNonStrict( DdManager * dd, DdNode ** pbColumns, int nColumns, DdNode * bVarsCol, DdNode ** pCVars, int nMulti, int * pSimple ); +/* collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root */ +extern st_table * Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLevel ); +/* collects the nodes under the cut starting from the given set of ADD nodes */ +extern int Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode ** pbCubes, int nNodes, DdNode ** paNodesRes, DdNode ** pbCubesRes, int CutLevel ); +/* find the profile of a DD (the number of edges crossing each level) */ +extern int Extra_ProfileWidth( DdManager * dd, DdNode * F, int * Profile, int CutLevel ); + +/*=== extraBddMisc.c ========================================================*/ + extern DdNode * Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute ); extern DdNode * Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f ); extern DdNode * Extra_bddRemapUp( DdManager * dd, DdNode * bF ); @@ -116,6 +181,21 @@ extern int * Extra_VectorSupportArray( DdManager * dd, DdNode ** F, int n extern DdNode * Extra_bddFindOneCube( DdManager * dd, DdNode * bF ); extern DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc ); extern DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ); +extern DdNode * Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst ); +extern DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f ); +extern int Extra_bddIsVar( DdNode * bFunc ); +extern DdNode * Extra_bddCreateAnd( DdManager * dd, int nVars ); +extern DdNode * Extra_bddCreateOr( DdManager * dd, int nVars ); +extern DdNode * Extra_bddCreateExor( DdManager * dd, int nVars ); +extern DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F ); +extern void Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut ); + +/*=== extraBddKmap.c ================================================================*/ + +/* displays the Karnaugh Map of a function */ +extern void Extra_PrintKMap( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nVars, DdNode ** XVars, int fSuppType, char ** pVarNames ); +/* displays the Karnaugh Map of a relation */ +extern void Extra_PrintKMapRelation( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nXVars, int nYVars, DdNode ** XVars, DdNode ** YVars ); /*=== extraBddSymm.c =================================================================*/ @@ -168,6 +248,46 @@ extern DdNode * extraZddTuplesFromBdd( DdManager * dd, DdNode * bVarsK, DdNo extern DdNode * Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS ); extern DdNode * extraZddSelectOneSubset( DdManager * dd, DdNode * zS ); +/*=== extraBddUnate.c =================================================================*/ + +typedef struct Extra_UnateVar_t_ Extra_UnateVar_t; +struct Extra_UnateVar_t_ { + unsigned iVar : 30; // index of the variable + unsigned Pos : 1; // 1 if positive unate + unsigned Neg : 1; // 1 if negative unate +}; + +typedef struct Extra_UnateInfo_t_ Extra_UnateInfo_t; +struct Extra_UnateInfo_t_ { + int nVars; // the number of variables in the support + int nVarsMax; // the number of variables in the DD manager + int nUnate; // the number of unate variables + Extra_UnateVar_t * pVars; // the array of variables present in the support +}; + +/* allocates the data structure */ +extern Extra_UnateInfo_t * Extra_UnateInfoAllocate( int nVars ); +/* deallocates the data structure */ +extern void Extra_UnateInfoDissolve( Extra_UnateInfo_t * ); +/* print the contents the data structure */ +extern void Extra_UnateInfoPrint( Extra_UnateInfo_t * ); +/* converts the ZDD into the Extra_SymmInfo_t structure */ +extern Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zUnate, DdNode * bVars ); +/* naive check of unateness of one variable */ +extern int Extra_bddCheckUnateNaive( DdManager * dd, DdNode * bF, int iVar ); + +/* computes the unateness information for the function */ +extern Extra_UnateInfo_t * Extra_UnateComputeFast( DdManager * dd, DdNode * bFunc ); +extern Extra_UnateInfo_t * Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc ); + +/* computes the classical symmetry information as a ZDD */ +extern DdNode * Extra_zddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars ); +extern DdNode * extraZddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars ); + +/* converts a set of variables into a set of singleton subsets */ +extern DdNode * Extra_zddGetSingletonsBoth( DdManager * dd, DdNode * bVars ); +extern DdNode * extraZddGetSingletonsBoth( DdManager * dd, DdNode * bVars ); + /*=== extraUtilBitMatrix.c ================================================================*/ typedef struct Extra_BitMat_t_ Extra_BitMat_t; @@ -191,7 +311,7 @@ extern int Extra_BitMatrixIsClique( Extra_BitMat_t * p ); /*=== extraUtilFile.c ========================================================*/ extern char * Extra_FileGetSimilarName( char * pFileNameWrong, char * pS1, char * pS2, char * pS3, char * pS4, char * pS5 ); -extern int Extra_FileNameCheckExtension( char * FileName, char * Extension ); +extern char * Extra_FileNameExtension( char * FileName ); extern char * Extra_FileNameAppend( char * pBase, char * pSuffix ); extern char * Extra_FileNameGeneric( char * FileName ); extern int Extra_FileSize( char * pFileName ); @@ -200,6 +320,9 @@ extern char * Extra_TimeStamp(); extern char * Extra_StringAppend( char * pStrGiven, char * pStrAdd ); extern unsigned Extra_ReadBinary( char * Buffer ); extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits ); +extern int Extra_ReadHexadecimal( unsigned Sign[], char * pString, int nVars ); +extern void Extra_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars ); +extern void Extra_PrintHexadecimalString( char * pString, unsigned Sign[], int nVars ); extern void Extra_PrintHex( FILE * pFile, unsigned uTruth, int nVars ); extern void Extra_PrintSymbols( FILE * pFile, char Char, int nTimes, int fPrintNewLine ); @@ -223,26 +346,28 @@ typedef struct Extra_MmStep_t_ Extra_MmStep_t; // fixed-size-block memory manager extern Extra_MmFixed_t * Extra_MmFixedStart( int nEntrySize ); -extern void Extra_MmFixedStop( Extra_MmFixed_t * p, int fVerbose ); +extern void Extra_MmFixedStop( Extra_MmFixed_t * p ); extern char * Extra_MmFixedEntryFetch( Extra_MmFixed_t * p ); extern void Extra_MmFixedEntryRecycle( Extra_MmFixed_t * p, char * pEntry ); extern void Extra_MmFixedRestart( Extra_MmFixed_t * p ); extern int Extra_MmFixedReadMemUsage( Extra_MmFixed_t * p ); +extern int Extra_MmFixedReadMaxEntriesUsed( Extra_MmFixed_t * p ); // flexible-size-block memory manager extern Extra_MmFlex_t * Extra_MmFlexStart(); -extern void Extra_MmFlexStop( Extra_MmFlex_t * p, int fVerbose ); +extern void Extra_MmFlexStop( Extra_MmFlex_t * p ); +extern void Extra_MmFlexPrint( Extra_MmFlex_t * p ); extern char * Extra_MmFlexEntryFetch( Extra_MmFlex_t * p, int nBytes ); extern int Extra_MmFlexReadMemUsage( Extra_MmFlex_t * p ); // hierarchical memory manager extern Extra_MmStep_t * Extra_MmStepStart( int nSteps ); -extern void Extra_MmStepStop( Extra_MmStep_t * p, int fVerbose ); +extern void Extra_MmStepStop( Extra_MmStep_t * p ); extern char * Extra_MmStepEntryFetch( Extra_MmStep_t * p, int nBytes ); extern void Extra_MmStepEntryRecycle( Extra_MmStep_t * p, char * pEntry, int nBytes ); extern int Extra_MmStepReadMemUsage( Extra_MmStep_t * p ); /*=== extraUtilMisc.c ========================================================*/ -/* finds the smallest integer larger of equal than the logarithm. */ +/* finds the smallest integer larger or equal than the logarithm */ extern int Extra_Base2Log( unsigned Num ); extern int Extra_Base2LogDouble( double Num ); extern int Extra_Base10Log( unsigned Num ); @@ -252,6 +377,8 @@ extern int Extra_Power3( int Num ); /* the number of combinations of k elements out of n */ extern int Extra_NumCombinations( int k, int n ); extern int * Extra_DeriveRadixCode( int Number, int Radix, int nDigits ); +/* counts the number of 1s in the bitstring */ +extern int Extra_CountOnes( unsigned char * pBytes, int nBytes ); /* the factorial of number */ extern int Extra_Factorial( int n ); /* the permutation of the given number of elements */ @@ -272,11 +399,14 @@ extern void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhas extern unsigned short Extra_TruthPerm4One( unsigned uTruth, int Phase ); extern unsigned Extra_TruthPerm5One( unsigned uTruth, int Phase ); extern void Extra_TruthPerm6One( unsigned * uTruth, int Phase, unsigned * uTruthRes ); +extern void Extra_TruthExpand( int nVars, int nWords, unsigned * puTruth, unsigned uPhase, unsigned * puTruthR ); /* precomputing tables for permutation mapping */ extern void ** Extra_ArrayAlloc( int nCols, int nRows, int Size ); extern unsigned short ** Extra_TruthPerm43(); extern unsigned ** Extra_TruthPerm53(); extern unsigned ** Extra_TruthPerm54(); +/* bubble sort for small number of entries */ +extern void Extra_BubbleSort( int Order[], int Costs[], int nSize, int fIncreasing ); /* for independence from CUDD */ extern unsigned int Cudd_PrimeCopy( unsigned int p ); @@ -294,31 +424,203 @@ extern void Extra_ProgressBarStop( ProgressBar * p ); extern void Extra_ProgressBarUpdate_int( ProgressBar * p, int nItemsCur, char * pString ); static inline void Extra_ProgressBarUpdate( ProgressBar * p, int nItemsCur, char * pString ) -{ if ( nItemsCur < *((int*)p) ) return; Extra_ProgressBarUpdate_int(p, nItemsCur, pString); } - -/*=== extraUtilIntVec.c ================================================================*/ - -typedef struct Extra_IntVec_t_ Extra_IntVec_t; -extern Extra_IntVec_t * Extra_IntVecAlloc( int nCap ); -extern Extra_IntVec_t * Extra_IntVecAllocArray( int * pArray, int nSize ); -extern Extra_IntVec_t * Extra_IntVecAllocArrayCopy( int * pArray, int nSize ); -extern Extra_IntVec_t * Extra_IntVecDup( Extra_IntVec_t * pVec ); -extern Extra_IntVec_t * Extra_IntVecDupArray( Extra_IntVec_t * pVec ); -extern void Extra_IntVecFree( Extra_IntVec_t * p ); -extern void Extra_IntVecFill( Extra_IntVec_t * p, int nSize, int Entry ); -extern int * Extra_IntVecReleaseArray( Extra_IntVec_t * p ); -extern int * Extra_IntVecReadArray( Extra_IntVec_t * p ); -extern int Extra_IntVecReadSize( Extra_IntVec_t * p ); -extern int Extra_IntVecReadEntry( Extra_IntVec_t * p, int i ); -extern int Extra_IntVecReadEntryLast( Extra_IntVec_t * p ); -extern void Extra_IntVecWriteEntry( Extra_IntVec_t * p, int i, int Entry ); -extern void Extra_IntVecGrow( Extra_IntVec_t * p, int nCapMin ); -extern void Extra_IntVecShrink( Extra_IntVec_t * p, int nSizeNew ); -extern void Extra_IntVecClear( Extra_IntVec_t * p ); -extern void Extra_IntVecPush( Extra_IntVec_t * p, int Entry ); -extern int Extra_IntVecPop( Extra_IntVec_t * p ); -extern void Extra_IntVecSort( Extra_IntVec_t * p ); +{ if ( p && nItemsCur < *((int*)p) ) return; Extra_ProgressBarUpdate_int(p, nItemsCur, pString); } + +/*=== extraUtilTruth.c ================================================================*/ + +static inline int Extra_Float2Int( float Val ) { return *((int *)&Val); } +static inline float Extra_Int2Float( int Num ) { return *((float *)&Num); } +static inline int Extra_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); } +static inline int Extra_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } + +static inline void Extra_TruthSetBit( unsigned * p, int Bit ) { p[Bit>>5] |= (1<<(Bit & 31)); } +static inline void Extra_TruthXorBit( unsigned * p, int Bit ) { p[Bit>>5] ^= (1<<(Bit & 31)); } +static inline int Extra_TruthHasBit( unsigned * p, int Bit ) { return (p[Bit>>5] & (1<<(Bit & 31))) > 0; } + +static inline int Extra_WordCountOnes( unsigned uWord ) +{ + uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555); + uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333); + uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F); + uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF); + return (uWord & 0x0000FFFF) + (uWord>>16); +} +static inline int Extra_TruthCountOnes( unsigned * pIn, int nVars ) +{ + int w, Counter = 0; + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + Counter += Extra_WordCountOnes(pIn[w]); + return Counter; +} +static inline int Extra_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars ) +{ + int w; + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + if ( pIn0[w] != pIn1[w] ) + return 0; + return 1; +} +static inline int Extra_TruthIsConst0( unsigned * pIn, int nVars ) +{ + int w; + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + if ( pIn[w] ) + return 0; + return 1; +} +static inline int Extra_TruthIsConst1( unsigned * pIn, int nVars ) +{ + int w; + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + if ( pIn[w] != ~(unsigned)0 ) + return 0; + return 1; +} +static inline int Extra_TruthIsImply( unsigned * pIn1, unsigned * pIn2, int nVars ) +{ + int w; + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + if ( pIn1[w] & ~pIn2[w] ) + return 0; + return 1; +} +static inline void Extra_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars ) +{ + int w; + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = pIn[w]; +} +static inline void Extra_TruthClear( unsigned * pOut, int nVars ) +{ + int w; + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = 0; +} +static inline void Extra_TruthFill( unsigned * pOut, int nVars ) +{ + int w; + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = ~(unsigned)0; +} +static inline void Extra_TruthNot( unsigned * pOut, unsigned * pIn, int nVars ) +{ + int w; + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = ~pIn[w]; +} +static inline void Extra_TruthAnd( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars ) +{ + int w; + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = pIn0[w] & pIn1[w]; +} +static inline void Extra_TruthOr( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars ) +{ + int w; + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = pIn0[w] | pIn1[w]; +} +static inline void Extra_TruthSharp( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars ) +{ + int w; + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = pIn0[w] & ~pIn1[w]; +} +static inline void Extra_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars ) +{ + int w; + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = ~(pIn0[w] & pIn1[w]); +} +static inline void Extra_TruthAndPhase( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars, int fCompl0, int fCompl1 ) +{ + int w; + if ( fCompl0 && fCompl1 ) + { + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = ~(pIn0[w] | pIn1[w]); + } + else if ( fCompl0 && !fCompl1 ) + { + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = ~pIn0[w] & pIn1[w]; + } + else if ( !fCompl0 && fCompl1 ) + { + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = pIn0[w] & ~pIn1[w]; + } + else // if ( !fCompl0 && !fCompl1 ) + { + for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = pIn0[w] & pIn1[w]; + } +} + +extern unsigned ** Extra_TruthElementary( int nVars ); +extern void Extra_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int Start ); +extern void Extra_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase ); +extern void Extra_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase ); +extern int Extra_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar ); +extern int Extra_TruthSupportSize( unsigned * pTruth, int nVars ); +extern int Extra_TruthSupport( unsigned * pTruth, int nVars ); +extern void Extra_TruthCofactor0( unsigned * pTruth, int nVars, int iVar ); +extern void Extra_TruthCofactor1( unsigned * pTruth, int nVars, int iVar ); +extern void Extra_TruthExist( unsigned * pTruth, int nVars, int iVar ); +extern void Extra_TruthForall( unsigned * pTruth, int nVars, int iVar ); +extern void Extra_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar ); +extern void Extra_TruthChangePhase( unsigned * pTruth, int nVars, int iVar ); +extern int Extra_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin ); +extern void Extra_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore ); +extern unsigned Extra_TruthHash( unsigned * pIn, int nWords ); +extern unsigned Extra_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore ); + +/*=== extraUtilUtil.c ================================================================*/ + +#ifndef ABS +#define ABS(a) ((a) < 0 ? -(a) : (a)) +#endif + +#ifndef MAX +#define MAX(a,b) ((a) > (b) ? (a) : (b)) +#endif + +#ifndef MIN +#define MIN(a,b) ((a) < (b) ? (a) : (b)) +#endif + +#ifndef ALLOC +#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num))) +#endif + +#ifndef FREE +#define FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0) +#endif + +#ifndef REALLOC +#define REALLOC(type, obj, num) \ + ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \ + ((type *) malloc(sizeof(type) * (num)))) +#endif + + +extern long Extra_CpuTime(); +extern int Extra_GetSoftDataLimit(); +extern void Extra_UtilGetoptReset(); +extern int Extra_UtilGetopt( int argc, char *argv[], char *optstring ); +extern char * Extra_UtilPrintTime( long t ); +extern char * Extra_UtilStrsav( char *s ); +extern char * Extra_UtilTildeExpand( char *fname ); +extern char * Extra_UtilFileSearch( char *file, char *path, char *mode ); +extern void (*Extra_UtilMMoutOfMemory)(); + +extern char * globalUtilOptarg; +extern int globalUtilOptind; /**AutomaticEnd***************************************************************/ +#ifdef __cplusplus +} +#endif + #endif /* __EXTRA_H__ */ |