abc70930: src/misc/extra/extra.h Source File

00001 
00029 #ifndef __EXTRA_H__
00030 #define __EXTRA_H__
00031 
00032 #ifdef __cplusplus
00033 extern "C" {
00034 #endif
00035 
00036 #ifdef _WIN32
00037 #define inline __inline // compatible with MS VS 6.0
00038 #endif
00039 
00040 /*---------------------------------------------------------------------------*/
00041 /* Nested includes                                                           */
00042 /*---------------------------------------------------------------------------*/
00043 
00044 // this include should be the first one in the list
00045 // it is used to catch memory leaks on Windows
00046 #include "leaks.h"
00047 
00048 #include <stdio.h>
00049 #include <stdlib.h>
00050 #include <string.h>
00051 #include <assert.h>
00052 #include <time.h>
00053 #include "st.h"
00054 #include "cuddInt.h"
00055 
00056 /*---------------------------------------------------------------------------*/
00057 /* Constant declarations                                                     */
00058 /*---------------------------------------------------------------------------*/
00059 
00060 /*---------------------------------------------------------------------------*/
00061 /* Stucture declarations                                                     */
00062 /*---------------------------------------------------------------------------*/
00063 
00064 /*---------------------------------------------------------------------------*/
00065 /* Type declarations                                                         */
00066 /*---------------------------------------------------------------------------*/
00067 
00068 /*---------------------------------------------------------------------------*/
00069 /* Variable declarations                                                     */
00070 /*---------------------------------------------------------------------------*/
00071 
00072 /*---------------------------------------------------------------------------*/
00073 /* Macro declarations                                                        */
00074 /*---------------------------------------------------------------------------*/
00075 
00076 typedef unsigned char      uint8;
00077 typedef unsigned short     uint16;
00078 typedef unsigned int       uint32;
00079 #ifdef WIN32
00080 typedef unsigned __int64   uint64;
00081 #else
00082 typedef unsigned long long uint64;
00083 #endif
00084 
00085 /* constants of the manager */
00086 #define     b0     Cudd_Not((dd)->one)
00087 #define     b1              (dd)->one
00088 #define     z0              (dd)->zero
00089 #define     z1              (dd)->one
00090 #define     a0              (dd)->zero
00091 #define     a1              (dd)->one
00092 
00093 // hash key macros
00094 #define hashKey1(a,TSIZE) \
00095 ((unsigned)(a) % TSIZE)
00096 
00097 #define hashKey2(a,b,TSIZE) \
00098 (((unsigned)(a) + (unsigned)(b) * DD_P1) % TSIZE)
00099 
00100 #define hashKey3(a,b,c,TSIZE) \
00101 (((((unsigned)(a) + (unsigned)(b)) * DD_P1 + (unsigned)(c)) * DD_P2 ) % TSIZE)
00102 
00103 #define hashKey4(a,b,c,d,TSIZE) \
00104 ((((((unsigned)(a) + (unsigned)(b)) * DD_P1 + (unsigned)(c)) * DD_P2 + \
00105    (unsigned)(d)) * DD_P3) % TSIZE)
00106 
00107 #define hashKey5(a,b,c,d,e,TSIZE) \
00108 (((((((unsigned)(a) + (unsigned)(b)) * DD_P1 + (unsigned)(c)) * DD_P2 + \
00109    (unsigned)(d)) * DD_P3 + (unsigned)(e)) * DD_P1) % TSIZE)
00110 
00111 #ifndef PRT
00112 #define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
00113 #define PRTn(a,t)  printf("%s = ", (a)); printf("%6.2f sec  ", (float)(t)/(float)(CLOCKS_PER_SEC))
00114 #endif
00115 
00116 #ifndef PRTP
00117 #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)
00118 #endif
00119 
00120 /*===========================================================================*/
00121 /*     Various Utilities                                                     */
00122 /*===========================================================================*/
00123 
00124 /*=== extraBddAuto.c ========================================================*/
00125 
00126 extern DdNode *     Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc );
00127 extern DdNode *     Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG );
00128 extern DdNode *      extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG );
00129 extern DdNode *     Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc );
00130 extern DdNode *      extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc );
00131 extern DdNode *     Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc );
00132 extern DdNode *      extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc );
00133 
00134 extern DdNode *     Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace );
00135 extern DdNode *      extraBddSpaceCanonVars( DdManager * dd, DdNode * bSpace );
00136 
00137 extern DdNode *     Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace );
00138 extern DdNode *     Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace );
00139 extern DdNode *      extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace );
00140 extern DdNode *     Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace );
00141 extern DdNode *      extraBddSpaceEquationsPos( DdManager * dd, DdNode * bSpace );
00142 
00143 extern DdNode *     Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA );
00144 extern DdNode *      extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA );
00145 extern DdNode *     Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA );
00146 extern DdNode *      extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA );
00147 
00148 extern DdNode *     Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars );
00149 extern DdNode **    Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations );
00150 
00151 /*=== extraBddCas.c =============================================================*/
00152 
00153 /* performs the binary encoding of the set of function using the given vars */
00154 extern DdNode *     Extra_bddEncodingBinary( DdManager * dd, DdNode ** pbFuncs, int nFuncs, DdNode ** pbVars, int nVars );
00155 /* solves the column encoding problem using a sophisticated method */
00156 extern DdNode *     Extra_bddEncodingNonStrict( DdManager * dd, DdNode ** pbColumns, int nColumns, DdNode * bVarsCol, DdNode ** pCVars, int nMulti, int * pSimple );
00157 /* collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root */
00158 extern st_table *   Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLevel );
00159 /* collects the nodes under the cut starting from the given set of ADD nodes */
00160 extern int          Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode ** pbCubes, int nNodes, DdNode ** paNodesRes, DdNode ** pbCubesRes, int CutLevel );
00161 /* find the profile of a DD (the number of edges crossing each level) */
00162 extern int          Extra_ProfileWidth( DdManager * dd, DdNode * F, int * Profile, int CutLevel );
00163 
00164 /*=== extraBddMisc.c ========================================================*/
00165 
00166 extern DdNode *     Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );
00167 extern DdNode *     Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f );
00168 extern DdNode *     Extra_bddRemapUp( DdManager * dd, DdNode * bF );
00169 extern DdNode *     Extra_bddMove( DdManager * dd, DdNode * bF, int fShiftUp );
00170 extern DdNode *     extraBddMove( DdManager * dd, DdNode * bF, DdNode * bFlag );
00171 extern void         Extra_StopManager( DdManager * dd );
00172 extern void         Extra_bddPrint( DdManager * dd, DdNode * F );
00173 extern void         extraDecomposeCover( DdManager* dd, DdNode*  zC, DdNode** zC0, DdNode** zC1, DdNode** zC2 );
00174 extern int          Extra_bddSuppSize( DdManager * dd, DdNode * bSupp );
00175 extern int          Extra_bddSuppContainVar( DdManager * dd, DdNode * bS, DdNode * bVar );
00176 extern int          Extra_bddSuppOverlapping( DdManager * dd, DdNode * S1, DdNode * S2 );
00177 extern int          Extra_bddSuppDifferentVars( DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax );
00178 extern int          Extra_bddSuppCheckContainment( DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall );
00179 extern int *        Extra_SupportArray( DdManager * dd, DdNode * F, int * support );
00180 extern int *        Extra_VectorSupportArray( DdManager * dd, DdNode ** F, int n, int * support );
00181 extern DdNode *     Extra_bddFindOneCube( DdManager * dd, DdNode * bF );
00182 extern DdNode *     Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc );
00183 extern DdNode *     Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );
00184 extern DdNode *     Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst );
00185 extern DdNode *     Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f );
00186 extern int          Extra_bddIsVar( DdNode * bFunc );
00187 extern DdNode *     Extra_bddCreateAnd( DdManager * dd, int nVars );
00188 extern DdNode *     Extra_bddCreateOr( DdManager * dd, int nVars );
00189 extern DdNode *     Extra_bddCreateExor( DdManager * dd, int nVars );
00190 extern DdNode *     Extra_zddPrimes( DdManager * dd, DdNode * F );
00191 extern void         Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut );
00192 
00193 /*=== extraBddKmap.c ================================================================*/
00194 
00195 /* displays the Karnaugh Map of a function */
00196 extern void        Extra_PrintKMap( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nVars, DdNode ** XVars, int fSuppType, char ** pVarNames );
00197 /* displays the Karnaugh Map of a relation */
00198 extern void        Extra_PrintKMapRelation( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nXVars, int nYVars, DdNode ** XVars, DdNode ** YVars );
00199 
00200 /*=== extraBddSymm.c =================================================================*/
00201 
00202 typedef struct Extra_SymmInfo_t_  Extra_SymmInfo_t;
00203 struct Extra_SymmInfo_t_ {
00204     int nVars;      // the number of variables in the support
00205     int nVarsMax;   // the number of variables in the DD manager
00206     int nSymms;     // the number of pair-wise symmetries
00207     int nNodes;     // the number of nodes in a ZDD (if applicable)
00208     int * pVars;    // the list of all variables present in the support
00209     char ** pSymms; // the symmetry information
00210 };
00211 
00212 /* computes the classical symmetry information for the function - recursive */
00213 extern Extra_SymmInfo_t *  Extra_SymmPairsCompute( DdManager * dd, DdNode * bFunc );
00214 /* computes the classical symmetry information for the function - using naive approach */
00215 extern Extra_SymmInfo_t *  Extra_SymmPairsComputeNaive( DdManager * dd, DdNode * bFunc );
00216 extern int         Extra_bddCheckVarsSymmetricNaive( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
00217 
00218 /* allocates the data structure */
00219 extern Extra_SymmInfo_t *  Extra_SymmPairsAllocate( int nVars );
00220 /* deallocates the data structure */
00221 extern void        Extra_SymmPairsDissolve( Extra_SymmInfo_t * );
00222 /* print the contents the data structure */
00223 extern void        Extra_SymmPairsPrint( Extra_SymmInfo_t * );
00224 /* converts the ZDD into the Extra_SymmInfo_t structure */
00225 extern Extra_SymmInfo_t *  Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bVars );
00226 
00227 /* computes the classical symmetry information as a ZDD */
00228 extern DdNode *    Extra_zddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
00229 extern DdNode *     extraZddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
00230 /* returns a singleton-set ZDD containing all variables that are symmetric with the given one */
00231 extern DdNode *    Extra_zddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
00232 extern DdNode *     extraZddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
00233 /* converts a set of variables into a set of singleton subsets */
00234 extern DdNode *    Extra_zddGetSingletons( DdManager * dd, DdNode * bVars );
00235 extern DdNode *     extraZddGetSingletons( DdManager * dd, DdNode * bVars );
00236 /* filters the set of variables using the support of the function */
00237 extern DdNode *    Extra_bddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
00238 extern DdNode *     extraBddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
00239 
00240 /* checks the possibility that the two vars are symmetric */
00241 extern int         Extra_bddCheckVarsSymmetric( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
00242 extern DdNode *     extraBddCheckVarsSymmetric( DdManager * dd, DdNode * bF, DdNode * bVars );
00243 
00244 /* build the set of all tuples of K variables out of N from the BDD cube */
00245 extern DdNode *    Extra_zddTuplesFromBdd( DdManager * dd, int K, DdNode * bVarsN );
00246 extern DdNode *     extraZddTuplesFromBdd( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN );
00247 /* selects one subset from a ZDD representing the set of subsets */
00248 extern DdNode *    Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS );
00249 extern DdNode *     extraZddSelectOneSubset( DdManager * dd, DdNode * zS );
00250 
00251 /*=== extraBddUnate.c =================================================================*/
00252 
00253 typedef struct Extra_UnateVar_t_  Extra_UnateVar_t;
00254 struct Extra_UnateVar_t_ {
00255     unsigned    iVar : 30;  // index of the variable
00256     unsigned    Pos  :  1;  // 1 if positive unate
00257     unsigned    Neg  :  1;  // 1 if negative unate
00258 };
00259 
00260 typedef struct Extra_UnateInfo_t_  Extra_UnateInfo_t;
00261 struct Extra_UnateInfo_t_ {
00262     int nVars;      // the number of variables in the support
00263     int nVarsMax;   // the number of variables in the DD manager
00264     int nUnate;     // the number of unate variables
00265     Extra_UnateVar_t * pVars;    // the array of variables present in the support
00266 };
00267 
00268 /* allocates the data structure */
00269 extern Extra_UnateInfo_t *  Extra_UnateInfoAllocate( int nVars );
00270 /* deallocates the data structure */
00271 extern void        Extra_UnateInfoDissolve( Extra_UnateInfo_t * );
00272 /* print the contents the data structure */
00273 extern void        Extra_UnateInfoPrint( Extra_UnateInfo_t * );
00274 /* converts the ZDD into the Extra_SymmInfo_t structure */
00275 extern Extra_UnateInfo_t *  Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zUnate, DdNode * bVars );
00276 /* naive check of unateness of one variable */
00277 extern int         Extra_bddCheckUnateNaive( DdManager * dd, DdNode * bF, int iVar );
00278 
00279 /* computes the unateness information for the function */
00280 extern Extra_UnateInfo_t *  Extra_UnateComputeFast( DdManager * dd, DdNode * bFunc );
00281 extern Extra_UnateInfo_t *  Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc );
00282 
00283 /* computes the classical symmetry information as a ZDD */
00284 extern DdNode *    Extra_zddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
00285 extern DdNode *     extraZddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
00286 
00287 /* converts a set of variables into a set of singleton subsets */
00288 extern DdNode *    Extra_zddGetSingletonsBoth( DdManager * dd, DdNode * bVars );
00289 extern DdNode *     extraZddGetSingletonsBoth( DdManager * dd, DdNode * bVars );
00290 
00291 /*=== extraUtilBitMatrix.c ================================================================*/
00292 
00293 typedef struct Extra_BitMat_t_ Extra_BitMat_t;
00294 extern Extra_BitMat_t * Extra_BitMatrixStart( int nSize );
00295 extern void         Extra_BitMatrixClean( Extra_BitMat_t * p );
00296 extern void         Extra_BitMatrixStop( Extra_BitMat_t * p );
00297 extern void         Extra_BitMatrixPrint( Extra_BitMat_t * p );
00298 extern int          Extra_BitMatrixReadSize( Extra_BitMat_t * p );
00299 extern void         Extra_BitMatrixInsert1( Extra_BitMat_t * p, int i, int k );
00300 extern int          Extra_BitMatrixLookup1( Extra_BitMat_t * p, int i, int k );
00301 extern void         Extra_BitMatrixDelete1( Extra_BitMat_t * p, int i, int k );
00302 extern void         Extra_BitMatrixInsert2( Extra_BitMat_t * p, int i, int k );
00303 extern int          Extra_BitMatrixLookup2( Extra_BitMat_t * p, int i, int k );
00304 extern void         Extra_BitMatrixDelete2( Extra_BitMat_t * p, int i, int k );
00305 extern void         Extra_BitMatrixOr( Extra_BitMat_t * p, int i, unsigned * pInfo );
00306 extern void         Extra_BitMatrixOrTwo( Extra_BitMat_t * p, int i, int j );
00307 extern int          Extra_BitMatrixCountOnesUpper( Extra_BitMat_t * p );
00308 extern int          Extra_BitMatrixIsDisjoint( Extra_BitMat_t * p1, Extra_BitMat_t * p2 );
00309 extern int          Extra_BitMatrixIsClique( Extra_BitMat_t * p );
00310 
00311 /*=== extraUtilFile.c ========================================================*/
00312 
00313 extern char *       Extra_FileGetSimilarName( char * pFileNameWrong, char * pS1, char * pS2, char * pS3, char * pS4, char * pS5 );
00314 extern char *       Extra_FileNameExtension( char * FileName );
00315 extern char *       Extra_FileNameAppend( char * pBase, char * pSuffix );
00316 extern char *       Extra_FileNameGeneric( char * FileName );
00317 extern int          Extra_FileSize( char * pFileName );
00318 extern char *       Extra_FileRead( FILE * pFile );
00319 extern char *       Extra_TimeStamp();
00320 extern char *       Extra_StringAppend( char * pStrGiven, char * pStrAdd );
00321 extern unsigned     Extra_ReadBinary( char * Buffer );
00322 extern void         Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
00323 extern int          Extra_ReadHexadecimal( unsigned Sign[], char * pString, int nVars );
00324 extern void         Extra_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars );
00325 extern void         Extra_PrintHexadecimalString( char * pString, unsigned Sign[], int nVars );
00326 extern void         Extra_PrintHex( FILE * pFile, unsigned uTruth, int nVars );
00327 extern void         Extra_PrintSymbols( FILE * pFile, char Char, int nTimes, int fPrintNewLine );
00328 
00329 /*=== extraUtilReader.c ========================================================*/
00330 
00331 typedef struct Extra_FileReader_t_ Extra_FileReader_t;
00332 extern Extra_FileReader_t * Extra_FileReaderAlloc( char * pFileName, 
00333     char * pCharsComment, char * pCharsStop, char * pCharsClean );
00334 extern void         Extra_FileReaderFree( Extra_FileReader_t * p );
00335 extern char *       Extra_FileReaderGetFileName( Extra_FileReader_t * p );
00336 extern int          Extra_FileReaderGetFileSize( Extra_FileReader_t * p );
00337 extern int          Extra_FileReaderGetCurPosition( Extra_FileReader_t * p );
00338 extern void *       Extra_FileReaderGetTokens( Extra_FileReader_t * p );
00339 extern int          Extra_FileReaderGetLineNumber( Extra_FileReader_t * p, int iToken );
00340 
00341 /*=== extraUtilMemory.c ========================================================*/
00342 
00343 typedef struct Extra_MmFixed_t_    Extra_MmFixed_t;    
00344 typedef struct Extra_MmFlex_t_     Extra_MmFlex_t;     
00345 typedef struct Extra_MmStep_t_     Extra_MmStep_t;     
00346 
00347 // fixed-size-block memory manager
00348 extern Extra_MmFixed_t *  Extra_MmFixedStart( int nEntrySize );
00349 extern void        Extra_MmFixedStop( Extra_MmFixed_t * p );
00350 extern char *      Extra_MmFixedEntryFetch( Extra_MmFixed_t * p );
00351 extern void        Extra_MmFixedEntryRecycle( Extra_MmFixed_t * p, char * pEntry );
00352 extern void        Extra_MmFixedRestart( Extra_MmFixed_t * p );
00353 extern int         Extra_MmFixedReadMemUsage( Extra_MmFixed_t * p );
00354 extern int         Extra_MmFixedReadMaxEntriesUsed( Extra_MmFixed_t * p );
00355 // flexible-size-block memory manager
00356 extern Extra_MmFlex_t * Extra_MmFlexStart();
00357 extern void        Extra_MmFlexStop( Extra_MmFlex_t * p );
00358 extern void        Extra_MmFlexPrint( Extra_MmFlex_t * p );
00359 extern char *      Extra_MmFlexEntryFetch( Extra_MmFlex_t * p, int nBytes );
00360 extern int         Extra_MmFlexReadMemUsage( Extra_MmFlex_t * p );
00361 // hierarchical memory manager
00362 extern Extra_MmStep_t * Extra_MmStepStart( int nSteps );
00363 extern void        Extra_MmStepStop( Extra_MmStep_t * p );
00364 extern char *      Extra_MmStepEntryFetch( Extra_MmStep_t * p, int nBytes );
00365 extern void        Extra_MmStepEntryRecycle( Extra_MmStep_t * p, char * pEntry, int nBytes );
00366 extern int         Extra_MmStepReadMemUsage( Extra_MmStep_t * p );
00367 
00368 /*=== extraUtilMisc.c ========================================================*/
00369 
00370 /* finds the smallest integer larger or equal than the logarithm */
00371 extern int         Extra_Base2Log( unsigned Num );
00372 extern int         Extra_Base2LogDouble( double Num );
00373 extern int         Extra_Base10Log( unsigned Num );
00374 /* returns the power of two as a double */
00375 extern double      Extra_Power2( int Num );
00376 extern int         Extra_Power3( int Num );
00377 /* the number of combinations of k elements out of n */
00378 extern int         Extra_NumCombinations( int k, int n  );
00379 extern int *       Extra_DeriveRadixCode( int Number, int Radix, int nDigits );
00380 /* counts the number of 1s in the bitstring */
00381 extern int         Extra_CountOnes( unsigned char * pBytes, int nBytes );
00382 /* the factorial of number */
00383 extern int         Extra_Factorial( int n );
00384 /* the permutation of the given number of elements */
00385 extern char **     Extra_Permutations( int n );
00386 /* permutation and complementation of a truth table */
00387 unsigned           Extra_TruthPermute( unsigned Truth, char * pPerms, int nVars, int fReverse );
00388 unsigned           Extra_TruthPolarize( unsigned uTruth, int Polarity, int nVars );
00389 /* canonical forms of a truth table */
00390 extern unsigned    Extra_TruthCanonN( unsigned uTruth, int nVars );
00391 extern unsigned    Extra_TruthCanonNN( unsigned uTruth, int nVars );
00392 extern unsigned    Extra_TruthCanonP( unsigned uTruth, int nVars );
00393 extern unsigned    Extra_TruthCanonNP( unsigned uTruth, int nVars );
00394 extern unsigned    Extra_TruthCanonNPN( unsigned uTruth, int nVars );
00395 /* canonical forms of 4-variable functions */
00396 extern void        Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap );
00397 extern void        Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** ppCounters, int nPhasesMax );
00398 /* permutation mapping */
00399 extern unsigned short Extra_TruthPerm4One( unsigned uTruth, int Phase );
00400 extern unsigned    Extra_TruthPerm5One( unsigned uTruth, int Phase );
00401 extern void        Extra_TruthPerm6One( unsigned * uTruth, int Phase, unsigned * uTruthRes );
00402 extern void        Extra_TruthExpand( int nVars, int nWords, unsigned * puTruth, unsigned uPhase, unsigned * puTruthR );
00403 /* precomputing tables for permutation mapping */
00404 extern void **     Extra_ArrayAlloc( int nCols, int nRows, int Size );
00405 extern unsigned short ** Extra_TruthPerm43();
00406 extern unsigned ** Extra_TruthPerm53();
00407 extern unsigned ** Extra_TruthPerm54();
00408 /* bubble sort for small number of entries */
00409 extern void        Extra_BubbleSort( int Order[], int Costs[], int nSize, int fIncreasing );
00410 /* for independence from CUDD */
00411 extern unsigned int Cudd_PrimeCopy( unsigned int  p );
00412 
00413 /*=== extraUtilCanon.c ========================================================*/
00414 
00415 /* fast computation of N-canoninical form up to 6 inputs */
00416 extern int         Extra_TruthCanonFastN( int nVarsMax, int nVarsReal, unsigned * pt, unsigned ** pptRes, char ** ppfRes );
00417 
00418 /*=== extraUtilProgress.c ================================================================*/
00419 
00420 typedef struct ProgressBarStruct ProgressBar;
00421 
00422 extern ProgressBar * Extra_ProgressBarStart( FILE * pFile, int nItemsTotal );
00423 extern void        Extra_ProgressBarStop( ProgressBar * p );
00424 extern void        Extra_ProgressBarUpdate_int( ProgressBar * p, int nItemsCur, char * pString );
00425 
00426 static inline void Extra_ProgressBarUpdate( ProgressBar * p, int nItemsCur, char * pString ) 
00427 {  if ( p && nItemsCur < *((int*)p) ) return; Extra_ProgressBarUpdate_int(p, nItemsCur, pString); }
00428 
00429 /*=== extraUtilTruth.c ================================================================*/
00430 
00431 static inline int   Extra_Float2Int( float Val )     { return *((int *)&Val);               }
00432 static inline float Extra_Int2Float( int Num )       { return *((float *)&Num);             }
00433 static inline int   Extra_BitWordNum( int nBits )    { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0);  }
00434 static inline int   Extra_TruthWordNum( int nVars )  { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
00435 
00436 static inline void  Extra_TruthSetBit( unsigned * p, int Bit )   { p[Bit>>5] |= (1<<(Bit & 31));               }
00437 static inline void  Extra_TruthXorBit( unsigned * p, int Bit )   { p[Bit>>5] ^= (1<<(Bit & 31));               }
00438 static inline int   Extra_TruthHasBit( unsigned * p, int Bit )   { return (p[Bit>>5] & (1<<(Bit & 31))) > 0;   }
00439 
00440 static inline int Extra_WordCountOnes( unsigned uWord )
00441 {
00442     uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
00443     uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
00444     uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
00445     uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
00446     return  (uWord & 0x0000FFFF) + (uWord>>16);
00447 }
00448 static inline int Extra_TruthCountOnes( unsigned * pIn, int nVars )
00449 {
00450     int w, Counter = 0;
00451     for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00452         Counter += Extra_WordCountOnes(pIn[w]);
00453     return Counter;
00454 }
00455 static inline int Extra_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars )
00456 {
00457     int w;
00458     for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00459         if ( pIn0[w] != pIn1[w] )
00460             return 0;
00461     return 1;
00462 }
00463 static inline int Extra_TruthIsConst0( unsigned * pIn, int nVars )
00464 {
00465     int w;
00466     for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00467         if ( pIn[w] )
00468             return 0;
00469     return 1;
00470 }
00471 static inline int Extra_TruthIsConst1( unsigned * pIn, int nVars )
00472 {
00473     int w;
00474     for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00475         if ( pIn[w] != ~(unsigned)0 )
00476             return 0;
00477     return 1;
00478 }
00479 static inline int Extra_TruthIsImply( unsigned * pIn1, unsigned * pIn2, int nVars )
00480 {
00481     int w;
00482     for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00483         if ( pIn1[w] & ~pIn2[w] )
00484             return 0;
00485     return 1;
00486 }
00487 static inline void Extra_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
00488 {
00489     int w;
00490     for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00491         pOut[w] = pIn[w];
00492 }
00493 static inline void Extra_TruthClear( unsigned * pOut, int nVars )
00494 {
00495     int w;
00496     for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00497         pOut[w] = 0;
00498 }
00499 static inline void Extra_TruthFill( unsigned * pOut, int nVars )
00500 {
00501     int w;
00502     for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00503         pOut[w] = ~(unsigned)0;
00504 }
00505 static inline void Extra_TruthNot( unsigned * pOut, unsigned * pIn, int nVars )
00506 {
00507     int w;
00508     for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00509         pOut[w] = ~pIn[w];
00510 }
00511 static inline void Extra_TruthAnd( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
00512 {
00513     int w;
00514     for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00515         pOut[w] = pIn0[w] & pIn1[w];
00516 }
00517 static inline void Extra_TruthOr( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
00518 {
00519     int w;
00520     for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00521         pOut[w] = pIn0[w] | pIn1[w];
00522 }
00523 static inline void Extra_TruthSharp( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
00524 {
00525     int w;
00526     for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00527         pOut[w] = pIn0[w] & ~pIn1[w];
00528 }
00529 static inline void Extra_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
00530 {
00531     int w;
00532     for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00533         pOut[w] = ~(pIn0[w] & pIn1[w]);
00534 }
00535 static inline void Extra_TruthAndPhase( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars, int fCompl0, int fCompl1 )
00536 {
00537     int w;
00538     if ( fCompl0 && fCompl1 )
00539     {
00540         for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00541             pOut[w] = ~(pIn0[w] | pIn1[w]);
00542     }
00543     else if ( fCompl0 && !fCompl1 )
00544     {
00545         for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00546             pOut[w] = ~pIn0[w] & pIn1[w];
00547     }
00548     else if ( !fCompl0 && fCompl1 )
00549     {
00550         for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00551             pOut[w] = pIn0[w] & ~pIn1[w];
00552     }
00553     else // if ( !fCompl0 && !fCompl1 )
00554     {
00555         for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
00556             pOut[w] = pIn0[w] & pIn1[w];
00557     }
00558 }
00559 
00560 extern unsigned ** Extra_TruthElementary( int nVars );
00561 extern void        Extra_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int Start );
00562 extern void        Extra_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
00563 extern void        Extra_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
00564 extern int         Extra_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar );
00565 extern int         Extra_TruthSupportSize( unsigned * pTruth, int nVars );
00566 extern int         Extra_TruthSupport( unsigned * pTruth, int nVars );
00567 extern void        Extra_TruthCofactor0( unsigned * pTruth, int nVars, int iVar );
00568 extern void        Extra_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
00569 extern void        Extra_TruthExist( unsigned * pTruth, int nVars, int iVar );
00570 extern void        Extra_TruthForall( unsigned * pTruth, int nVars, int iVar );
00571 extern void        Extra_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
00572 extern void        Extra_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
00573 extern int         Extra_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
00574 extern void        Extra_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
00575 extern unsigned    Extra_TruthHash( unsigned * pIn, int nWords );
00576 extern unsigned    Extra_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore );
00577 
00578 /*=== extraUtilUtil.c ================================================================*/
00579 
00580 #ifndef ABS
00581 #define ABS(a)                  ((a) < 0 ? -(a) : (a))
00582 #endif
00583 
00584 #ifndef MAX
00585 #define MAX(a,b)                ((a) > (b) ? (a) : (b))
00586 #endif
00587 
00588 #ifndef MIN
00589 #define MIN(a,b)                ((a) < (b) ? (a) : (b))
00590 #endif
00591 
00592 #ifndef ALLOC
00593 #define ALLOC(type, num)         ((type *) malloc(sizeof(type) * (num)))
00594 #endif
00595 
00596 #ifndef FREE
00597 #define FREE(obj)                    ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
00598 #endif
00599 
00600 #ifndef REALLOC
00601 #define REALLOC(type, obj, num) \
00602         ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
00603              ((type *) malloc(sizeof(type) * (num))))
00604 #endif
00605 
00606 
00607 extern long        Extra_CpuTime();
00608 extern int         Extra_GetSoftDataLimit();
00609 extern void        Extra_UtilGetoptReset();
00610 extern int         Extra_UtilGetopt( int argc, char *argv[], char *optstring );
00611 extern char *      Extra_UtilPrintTime( long t );
00612 extern char *      Extra_UtilStrsav( char *s );
00613 extern char *      Extra_UtilTildeExpand( char *fname );
00614 extern char *      Extra_UtilFileSearch( char *file, char *path, char *mode );
00615 extern void        (*Extra_UtilMMoutOfMemory)();
00616 
00617 extern char *      globalUtilOptarg;
00618 extern int         globalUtilOptind;
00619 
00622 #ifdef __cplusplus
00623 }
00624 #endif
00625 
00626 #endif /* __EXTRA_H__ */