diff options
Diffstat (limited to 'src/misc/extra')
| -rw-r--r-- | src/misc/extra/extra.h | 364 | ||||
| -rw-r--r-- | src/misc/extra/extraBddAuto.c | 1558 | ||||
| -rw-r--r-- | src/misc/extra/extraBddCas.c | 1230 | ||||
| -rw-r--r-- | src/misc/extra/extraBddKmap.c | 783 | ||||
| -rw-r--r-- | src/misc/extra/extraBddMisc.c | 574 | ||||
| -rw-r--r-- | src/misc/extra/extraBddSymm.c | 2 | ||||
| -rw-r--r-- | src/misc/extra/extraBddUnate.c | 641 | ||||
| -rw-r--r-- | src/misc/extra/extraUtilBitMatrix.c | 2 | ||||
| -rw-r--r-- | src/misc/extra/extraUtilCanon.c | 24 | ||||
| -rw-r--r-- | src/misc/extra/extraUtilFile.c | 114 | ||||
| -rw-r--r-- | src/misc/extra/extraUtilMemory.c | 103 | ||||
| -rw-r--r-- | src/misc/extra/extraUtilMisc.c | 805 | ||||
| -rw-r--r-- | src/misc/extra/extraUtilProgress.c | 30 | ||||
| -rw-r--r-- | src/misc/extra/extraUtilReader.c | 21 | ||||
| -rw-r--r-- | src/misc/extra/extraUtilTruth.c | 1148 | ||||
| -rw-r--r-- | src/misc/extra/extraUtilUtil.c | 356 | ||||
| -rw-r--r-- | src/misc/extra/module.make | 10 |
17 files changed, 98 insertions, 7667 deletions
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index 314257a2..f36b113f 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -29,10 +29,6 @@ #ifndef __EXTRA_H__ #define __EXTRA_H__ -#ifdef __cplusplus -extern "C" { -#endif - #ifdef _WIN32 #define inline __inline // compatible with MS VS 6.0 #endif @@ -41,15 +37,9 @@ extern "C" { /* 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" @@ -73,15 +63,6 @@ extern "C" { /* 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 @@ -110,59 +91,13 @@ typedef unsigned long long uint64; #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 */ /*===========================================================================*/ -/*=== 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 ========================================================*/ - +/*=== extraUtilBdd.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 ); @@ -181,21 +116,6 @@ 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 =================================================================*/ @@ -248,46 +168,6 @@ 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; @@ -311,7 +191,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 char * Extra_FileNameExtension( char * FileName ); +extern int Extra_FileNameCheckExtension( char * FileName, char * Extension ); extern char * Extra_FileNameAppend( char * pBase, char * pSuffix ); extern char * Extra_FileNameGeneric( char * FileName ); extern int Extra_FileSize( char * pFileName ); @@ -320,9 +200,6 @@ 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 ); @@ -346,28 +223,26 @@ 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 ); +extern void Extra_MmFixedStop( Extra_MmFixed_t * p, int fVerbose ); 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 ); -extern void Extra_MmFlexPrint( Extra_MmFlex_t * p ); +extern void Extra_MmFlexStop( Extra_MmFlex_t * p, int fVerbose ); 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 ); +extern void Extra_MmStepStop( Extra_MmStep_t * p, int fVerbose ); 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 or equal than the logarithm */ +/* finds the smallest integer larger of equal than the logarithm. */ extern int Extra_Base2Log( unsigned Num ); extern int Extra_Base2LogDouble( double Num ); extern int Extra_Base10Log( unsigned Num ); @@ -377,8 +252,6 @@ 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 */ @@ -399,14 +272,11 @@ 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 ); @@ -424,203 +294,31 @@ 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 ( 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; +{ 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 ); /**AutomaticEnd***************************************************************/ -#ifdef __cplusplus -} -#endif - #endif /* __EXTRA_H__ */ diff --git a/src/misc/extra/extraBddAuto.c b/src/misc/extra/extraBddAuto.c deleted file mode 100644 index 21a969ba..00000000 --- a/src/misc/extra/extraBddAuto.c +++ /dev/null @@ -1,1558 +0,0 @@ -/**CFile**************************************************************** - - FileName [extraBddAuto.c] - - PackageName [extra] - - Synopsis [Computation of autosymmetries.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 2.0. Started - September 1, 2003.] - - Revision [$Id: extraBddAuto.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $] - -***********************************************************************/ - -#include "extra.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -/**AutomaticEnd***************************************************************/ - - -/* - LinearSpace(f) = Space(f,f) - - Space(f,g) - { - if ( f = const ) - { - if ( f = g ) return 1; - else return 0; - } - if ( g = const ) return 0; - return x' * Space(fx',gx') * Space(fx,gx) + x * Space(fx',gx) * Space(fx,gx'); - } - - Equations(s) = Pos(s) + Neg(s); - - Pos(s) - { - if ( s = 0 ) return 1; - if ( s = 1 ) return 0; - if ( sx'= 0 ) return Pos(sx) + x; - if ( sx = 0 ) return Pos(sx'); - return 1 * [Pos(sx') & Pos(sx)] + x * [Pos(sx') & Neg(sx)]; - } - - Neg(s) - { - if ( s = 0 ) return 1; - if ( s = 1 ) return 0; - if ( sx'= 0 ) return Neg(sx); - if ( sx = 0 ) return Neg(sx') + x; - return 1 * [Neg(sx') & Neg(sx)] + x * [Neg(sx') & Pos(sx)]; - } - - - SpaceP(A) - { - if ( A = 0 ) return 1; - if ( A = 1 ) return 1; - return x' * SpaceP(Ax') * SpaceP(Ax) + x * SpaceP(Ax') * SpaceN(Ax); - } - - SpaceN(A) - { - if ( A = 0 ) return 1; - if ( A = 1 ) return 0; - return x' * SpaceN(Ax') * SpaceN(Ax) + x * SpaceN(Ax') * SpaceP(Ax); - } - - - LinInd(A) - { - if ( A = const ) return 1; - if ( !LinInd(Ax') ) return 0; - if ( !LinInd(Ax) ) return 0; - if ( LinSumOdd(Ax') & LinSumEven(Ax) != 0 ) return 0; - if ( LinSumEven(Ax') & LinSumEven(Ax) != 0 ) return 0; - return 1; - } - - LinSumOdd(A) - { - if ( A = 0 ) return 0; // Odd0 ---e-- Odd1 - if ( A = 1 ) return 1; // \ o - Odd0 = LinSumOdd(Ax'); // x is absent // \ - Even0 = LinSumEven(Ax'); // x is absent // / o - Odd1 = LinSumOdd(Ax); // x is present // Even0 ---e-- Even1 - Even1 = LinSumEven(Ax); // x is absent - return 1 * [Odd0 + ExorP(Odd0, Even1)] + x * [Odd1 + ExorP(Odd1, Even0)]; - } - - LinSumEven(A) - { - if ( A = 0 ) return 0; - if ( A = 1 ) return 0; - Odd0 = LinSumOdd(Ax'); // x is absent - Even0 = LinSumEven(Ax'); // x is absent - Odd1 = LinSumOdd(Ax); // x is present - Even1 = LinSumEven(Ax); // x is absent - return 1 * [Even0 + Even1 + ExorP(Even0, Even1)] + x * [ExorP(Odd0, Odd1)]; - } - -*/ - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc ) -{ - int * pSupport; - int * pPermute; - int * pPermuteBack; - DdNode ** pCompose; - DdNode * bCube, * bTemp; - DdNode * bSpace, * bFunc1, * bFunc2, * bSpaceShift; - int nSupp, Counter; - int i, lev; - - // get the support - pSupport = ALLOC( int, ddMax(dd->size,dd->sizeZ) ); - Extra_SupportArray( dd, bFunc, pSupport ); - nSupp = 0; - for ( i = 0; i < dd->size; i++ ) - if ( pSupport[i] ) - nSupp++; - - // make sure the manager has enough variables - if ( 2*nSupp > dd->size ) - { - printf( "Cannot derive linear space, because DD manager does not have enough variables.\n" ); - fflush( stdout ); - free( pSupport ); - return NULL; - } - - // create the permutation arrays - pPermute = ALLOC( int, dd->size ); - pPermuteBack = ALLOC( int, dd->size ); - pCompose = ALLOC( DdNode *, dd->size ); - for ( i = 0; i < dd->size; i++ ) - { - pPermute[i] = i; - pPermuteBack[i] = i; - pCompose[i] = dd->vars[i]; Cudd_Ref( pCompose[i] ); - } - - // remap the function in such a way that the variables are interleaved - Counter = 0; - bCube = b1; Cudd_Ref( bCube ); - for ( lev = 0; lev < dd->size; lev++ ) - if ( pSupport[ dd->invperm[lev] ] ) - { // var "dd->invperm[lev]" on level "lev" should go to level 2*Counter; - pPermute[ dd->invperm[lev] ] = dd->invperm[2*Counter]; - // var from level 2*Counter+1 should go back to the place of this var - pPermuteBack[ dd->invperm[2*Counter+1] ] = dd->invperm[lev]; - // the permutation should be defined in such a way that variable - // on level 2*Counter is replaced by an EXOR of itself and var on the next level - Cudd_Deref( pCompose[ dd->invperm[2*Counter] ] ); - pCompose[ dd->invperm[2*Counter] ] = - Cudd_bddXor( dd, dd->vars[ dd->invperm[2*Counter] ], dd->vars[ dd->invperm[2*Counter+1] ] ); - Cudd_Ref( pCompose[ dd->invperm[2*Counter] ] ); - // add this variable to the cube - bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[ dd->invperm[2*Counter] ] ); Cudd_Ref( bCube ); - Cudd_RecursiveDeref( dd, bTemp ); - // increment the counter - Counter ++; - } - - // permute the functions - bFunc1 = Cudd_bddPermute( dd, bFunc, pPermute ); Cudd_Ref( bFunc1 ); - // compose to gate the function depending on both vars - bFunc2 = Cudd_bddVectorCompose( dd, bFunc1, pCompose ); Cudd_Ref( bFunc2 ); - // gate the vector space - // L(a) = ForAll x [ F(x) = F(x+a) ] = Not( Exist x [ F(x) (+) F(x+a) ] ) - bSpaceShift = Cudd_bddXorExistAbstract( dd, bFunc1, bFunc2, bCube ); Cudd_Ref( bSpaceShift ); - bSpaceShift = Cudd_Not( bSpaceShift ); - // permute the space back into the original mapping - bSpace = Cudd_bddPermute( dd, bSpaceShift, pPermuteBack ); Cudd_Ref( bSpace ); - Cudd_RecursiveDeref( dd, bFunc1 ); - Cudd_RecursiveDeref( dd, bFunc2 ); - Cudd_RecursiveDeref( dd, bSpaceShift ); - Cudd_RecursiveDeref( dd, bCube ); - - for ( i = 0; i < dd->size; i++ ) - Cudd_RecursiveDeref( dd, pCompose[i] ); - free( pPermute ); - free( pPermuteBack ); - free( pCompose ); - free( pSupport ); - - Cudd_Deref( bSpace ); - return bSpace; -} - - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ) -{ - DdNode * bRes; - do { - dd->reordered = 0; - bRes = extraBddSpaceFromFunction( dd, bF, bG ); - } while (dd->reordered == 1); - return bRes; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc ) -{ - DdNode * bRes; - do { - dd->reordered = 0; - bRes = extraBddSpaceFromFunctionPos( dd, bFunc ); - } while (dd->reordered == 1); - return bRes; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc ) -{ - DdNode * bRes; - do { - dd->reordered = 0; - bRes = extraBddSpaceFromFunctionNeg( dd, bFunc ); - } while (dd->reordered == 1); - return bRes; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace ) -{ - DdNode * bRes; - do { - dd->reordered = 0; - bRes = extraBddSpaceCanonVars( dd, bSpace ); - } while (dd->reordered == 1); - return bRes; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars ) -{ - DdNode * bNegCube; - DdNode * bResult; - bNegCube = Extra_bddSupportNegativeCube( dd, bCanonVars ); Cudd_Ref( bNegCube ); - bResult = Cudd_Cofactor( dd, bFunc, bNegCube ); Cudd_Ref( bResult ); - Cudd_RecursiveDeref( dd, bNegCube ); - Cudd_Deref( bResult ); - return bResult; -} - - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace ) -{ - DdNode * zRes; - DdNode * zEquPos; - DdNode * zEquNeg; - zEquPos = Extra_bddSpaceEquationsPos( dd, bSpace ); Cudd_Ref( zEquPos ); - zEquNeg = Extra_bddSpaceEquationsNeg( dd, bSpace ); Cudd_Ref( zEquNeg ); - zRes = Cudd_zddUnion( dd, zEquPos, zEquNeg ); Cudd_Ref( zRes ); - Cudd_RecursiveDerefZdd( dd, zEquPos ); - Cudd_RecursiveDerefZdd( dd, zEquNeg ); - Cudd_Deref( zRes ); - return zRes; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace ) -{ - DdNode * zRes; - do { - dd->reordered = 0; - zRes = extraBddSpaceEquationsPos( dd, bSpace ); - } while (dd->reordered == 1); - return zRes; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace ) -{ - DdNode * zRes; - do { - dd->reordered = 0; - zRes = extraBddSpaceEquationsNeg( dd, bSpace ); - } while (dd->reordered == 1); - return zRes; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ) -{ - DdNode * bRes; - do { - dd->reordered = 0; - bRes = extraBddSpaceFromMatrixPos( dd, zA ); - } while (dd->reordered == 1); - return bRes; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ) -{ - DdNode * bRes; - do { - dd->reordered = 0; - bRes = extraBddSpaceFromMatrixNeg( dd, zA ); - } while (dd->reordered == 1); - return bRes; -} - -/**Function************************************************************* - - Synopsis [Counts the number of literals in one combination.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Extra_zddLitCountComb( DdManager * dd, DdNode * zComb ) -{ - int Counter; - if ( zComb == z0 ) - return 0; - Counter = 0; - for ( ; zComb != z1; zComb = cuddT(zComb) ) - Counter++; - return Counter; -} - -/**Function************************************************************* - - Synopsis [] - - Description [Returns the array of ZDDs with the number equal to the number of - vars in the DD manager. If the given var is non-canonical, this array contains - the referenced ZDD representing literals in the corresponding EXOR equation.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations ) -{ - DdNode ** pzRes; - int * pVarsNonCan; - DdNode * zEquRem; - int iVarNonCan; - DdNode * zExor, * zTemp; - - // get the set of non-canonical variables - pVarsNonCan = ALLOC( int, ddMax(dd->size,dd->sizeZ) ); - Extra_SupportArray( dd, bFuncRed, pVarsNonCan ); - - // allocate storage for the EXOR sets - pzRes = ALLOC( DdNode *, dd->size ); - memset( pzRes, 0, sizeof(DdNode *) * dd->size ); - - // go through all the equations - zEquRem = zEquations; Cudd_Ref( zEquRem ); - while ( zEquRem != z0 ) - { - // extract one product - zExor = Extra_zddSelectOneSubset( dd, zEquRem ); Cudd_Ref( zExor ); - // remove it from the set - zEquRem = Cudd_zddDiff( dd, zTemp = zEquRem, zExor ); Cudd_Ref( zEquRem ); - Cudd_RecursiveDerefZdd( dd, zTemp ); - - // locate the non-canonical variable - iVarNonCan = -1; - for ( zTemp = zExor; zTemp != z1; zTemp = cuddT(zTemp) ) - { - if ( pVarsNonCan[zTemp->index/2] == 1 ) - { - assert( iVarNonCan == -1 ); - iVarNonCan = zTemp->index/2; - } - } - assert( iVarNonCan != -1 ); - - if ( Extra_zddLitCountComb( dd, zExor ) > 1 ) - pzRes[ iVarNonCan ] = zExor; // takes ref - else - Cudd_RecursiveDerefZdd( dd, zExor ); - } - Cudd_RecursiveDerefZdd( dd, zEquRem ); - - free( pVarsNonCan ); - return pzRes; -} - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Performs the recursive steps of Extra_bddSpaceFromFunction.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ) -{ - DdNode * bRes; - DdNode * bFR, * bGR; - - bFR = Cudd_Regular( bF ); - bGR = Cudd_Regular( bG ); - if ( cuddIsConstant(bFR) ) - { - if ( bF == bG ) - return b1; - else - return b0; - } - if ( cuddIsConstant(bGR) ) - return b0; - // both bFunc and bCore are not constants - - // the operation is commutative - normalize the problem - if ( (unsigned)bF > (unsigned)bG ) - return extraBddSpaceFromFunction(dd, bG, bF); - - - if ( bRes = cuddCacheLookup2(dd, extraBddSpaceFromFunction, bF, bG) ) - return bRes; - else - { - DdNode * bF0, * bF1; - DdNode * bG0, * bG1; - DdNode * bTemp1, * bTemp2; - DdNode * bRes0, * bRes1; - int LevelF, LevelG; - int index; - - LevelF = dd->perm[bFR->index]; - LevelG = dd->perm[bGR->index]; - if ( LevelF <= LevelG ) - { - index = dd->invperm[LevelF]; - if ( bFR != bF ) - { - bF0 = Cudd_Not( cuddE(bFR) ); - bF1 = Cudd_Not( cuddT(bFR) ); - } - else - { - bF0 = cuddE(bFR); - bF1 = cuddT(bFR); - } - } - else - { - index = dd->invperm[LevelG]; - bF0 = bF1 = bF; - } - - if ( LevelG <= LevelF ) - { - if ( bGR != bG ) - { - bG0 = Cudd_Not( cuddE(bGR) ); - bG1 = Cudd_Not( cuddT(bGR) ); - } - else - { - bG0 = cuddE(bGR); - bG1 = cuddT(bGR); - } - } - else - bG0 = bG1 = bG; - - bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG0 ); - if ( bTemp1 == NULL ) - return NULL; - cuddRef( bTemp1 ); - - bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG1 ); - if ( bTemp2 == NULL ) - { - Cudd_RecursiveDeref( dd, bTemp1 ); - return NULL; - } - cuddRef( bTemp2 ); - - - bRes0 = cuddBddAndRecur( dd, bTemp1, bTemp2 ); - if ( bRes0 == NULL ) - { - Cudd_RecursiveDeref( dd, bTemp1 ); - Cudd_RecursiveDeref( dd, bTemp2 ); - return NULL; - } - cuddRef( bRes0 ); - Cudd_RecursiveDeref( dd, bTemp1 ); - Cudd_RecursiveDeref( dd, bTemp2 ); - - - bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG1 ); - if ( bTemp1 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - return NULL; - } - cuddRef( bTemp1 ); - - bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG0 ); - if ( bTemp2 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - Cudd_RecursiveDeref( dd, bTemp1 ); - return NULL; - } - cuddRef( bTemp2 ); - - bRes1 = cuddBddAndRecur( dd, bTemp1, bTemp2 ); - if ( bRes1 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - Cudd_RecursiveDeref( dd, bTemp1 ); - Cudd_RecursiveDeref( dd, bTemp2 ); - return NULL; - } - cuddRef( bRes1 ); - Cudd_RecursiveDeref( dd, bTemp1 ); - Cudd_RecursiveDeref( dd, bTemp2 ); - - - - // consider the case when Res0 and Res1 are the same node - if ( bRes0 == bRes1 ) - bRes = bRes1; - // consider the case when Res1 is complemented - else if ( Cudd_IsComplement(bRes1) ) - { - bRes = cuddUniqueInter(dd, index, Cudd_Not(bRes1), Cudd_Not(bRes0)); - if ( bRes == NULL ) - { - Cudd_RecursiveDeref(dd,bRes0); - Cudd_RecursiveDeref(dd,bRes1); - return NULL; - } - bRes = Cudd_Not(bRes); - } - else - { - bRes = cuddUniqueInter( dd, index, bRes1, bRes0 ); - if ( bRes == NULL ) - { - Cudd_RecursiveDeref(dd,bRes0); - Cudd_RecursiveDeref(dd,bRes1); - return NULL; - } - } - cuddDeref( bRes0 ); - cuddDeref( bRes1 ); - - // insert the result into cache - cuddCacheInsert2(dd, extraBddSpaceFromFunction, bF, bG, bRes); - return bRes; - } -} /* end of extraBddSpaceFromFunction */ - - - -/**Function************************************************************* - - Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bF ) -{ - DdNode * bRes, * bFR; - statLine( dd ); - - bFR = Cudd_Regular(bF); - if ( cuddIsConstant(bFR) ) - return b1; - - if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionPos, bF) ) - return bRes; - else - { - DdNode * bF0, * bF1; - DdNode * bPos0, * bPos1; - DdNode * bNeg0, * bNeg1; - DdNode * bRes0, * bRes1; - - if ( bFR != bF ) // bF is complemented - { - bF0 = Cudd_Not( cuddE(bFR) ); - bF1 = Cudd_Not( cuddT(bFR) ); - } - else - { - bF0 = cuddE(bFR); - bF1 = cuddT(bFR); - } - - - bPos0 = extraBddSpaceFromFunctionPos( dd, bF0 ); - if ( bPos0 == NULL ) - return NULL; - cuddRef( bPos0 ); - - bPos1 = extraBddSpaceFromFunctionPos( dd, bF1 ); - if ( bPos1 == NULL ) - { - Cudd_RecursiveDeref( dd, bPos0 ); - return NULL; - } - cuddRef( bPos1 ); - - bRes0 = cuddBddAndRecur( dd, bPos0, bPos1 ); - if ( bRes0 == NULL ) - { - Cudd_RecursiveDeref( dd, bPos0 ); - Cudd_RecursiveDeref( dd, bPos1 ); - return NULL; - } - cuddRef( bRes0 ); - Cudd_RecursiveDeref( dd, bPos0 ); - Cudd_RecursiveDeref( dd, bPos1 ); - - - bNeg0 = extraBddSpaceFromFunctionNeg( dd, bF0 ); - if ( bNeg0 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - return NULL; - } - cuddRef( bNeg0 ); - - bNeg1 = extraBddSpaceFromFunctionNeg( dd, bF1 ); - if ( bNeg1 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - Cudd_RecursiveDeref( dd, bNeg0 ); - return NULL; - } - cuddRef( bNeg1 ); - - bRes1 = cuddBddAndRecur( dd, bNeg0, bNeg1 ); - if ( bRes1 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - Cudd_RecursiveDeref( dd, bNeg0 ); - Cudd_RecursiveDeref( dd, bNeg1 ); - return NULL; - } - cuddRef( bRes1 ); - Cudd_RecursiveDeref( dd, bNeg0 ); - Cudd_RecursiveDeref( dd, bNeg1 ); - - - // consider the case when Res0 and Res1 are the same node - if ( bRes0 == bRes1 ) - bRes = bRes1; - // consider the case when Res1 is complemented - else if ( Cudd_IsComplement(bRes1) ) - { - bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) ); - if ( bRes == NULL ) - { - Cudd_RecursiveDeref(dd,bRes0); - Cudd_RecursiveDeref(dd,bRes1); - return NULL; - } - bRes = Cudd_Not(bRes); - } - else - { - bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 ); - if ( bRes == NULL ) - { - Cudd_RecursiveDeref(dd,bRes0); - Cudd_RecursiveDeref(dd,bRes1); - return NULL; - } - } - cuddDeref( bRes0 ); - cuddDeref( bRes1 ); - - cuddCacheInsert1( dd, extraBddSpaceFromFunctionPos, bF, bRes ); - return bRes; - } -} - - - -/**Function************************************************************* - - Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bF ) -{ - DdNode * bRes, * bFR; - statLine( dd ); - - bFR = Cudd_Regular(bF); - if ( cuddIsConstant(bFR) ) - return b0; - - if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionNeg, bF) ) - return bRes; - else - { - DdNode * bF0, * bF1; - DdNode * bPos0, * bPos1; - DdNode * bNeg0, * bNeg1; - DdNode * bRes0, * bRes1; - - if ( bFR != bF ) // bF is complemented - { - bF0 = Cudd_Not( cuddE(bFR) ); - bF1 = Cudd_Not( cuddT(bFR) ); - } - else - { - bF0 = cuddE(bFR); - bF1 = cuddT(bFR); - } - - - bPos0 = extraBddSpaceFromFunctionNeg( dd, bF0 ); - if ( bPos0 == NULL ) - return NULL; - cuddRef( bPos0 ); - - bPos1 = extraBddSpaceFromFunctionNeg( dd, bF1 ); - if ( bPos1 == NULL ) - { - Cudd_RecursiveDeref( dd, bPos0 ); - return NULL; - } - cuddRef( bPos1 ); - - bRes0 = cuddBddAndRecur( dd, bPos0, bPos1 ); - if ( bRes0 == NULL ) - { - Cudd_RecursiveDeref( dd, bPos0 ); - Cudd_RecursiveDeref( dd, bPos1 ); - return NULL; - } - cuddRef( bRes0 ); - Cudd_RecursiveDeref( dd, bPos0 ); - Cudd_RecursiveDeref( dd, bPos1 ); - - - bNeg0 = extraBddSpaceFromFunctionPos( dd, bF0 ); - if ( bNeg0 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - return NULL; - } - cuddRef( bNeg0 ); - - bNeg1 = extraBddSpaceFromFunctionPos( dd, bF1 ); - if ( bNeg1 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - Cudd_RecursiveDeref( dd, bNeg0 ); - return NULL; - } - cuddRef( bNeg1 ); - - bRes1 = cuddBddAndRecur( dd, bNeg0, bNeg1 ); - if ( bRes1 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - Cudd_RecursiveDeref( dd, bNeg0 ); - Cudd_RecursiveDeref( dd, bNeg1 ); - return NULL; - } - cuddRef( bRes1 ); - Cudd_RecursiveDeref( dd, bNeg0 ); - Cudd_RecursiveDeref( dd, bNeg1 ); - - - // consider the case when Res0 and Res1 are the same node - if ( bRes0 == bRes1 ) - bRes = bRes1; - // consider the case when Res1 is complemented - else if ( Cudd_IsComplement(bRes1) ) - { - bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) ); - if ( bRes == NULL ) - { - Cudd_RecursiveDeref(dd,bRes0); - Cudd_RecursiveDeref(dd,bRes1); - return NULL; - } - bRes = Cudd_Not(bRes); - } - else - { - bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 ); - if ( bRes == NULL ) - { - Cudd_RecursiveDeref(dd,bRes0); - Cudd_RecursiveDeref(dd,bRes1); - return NULL; - } - } - cuddDeref( bRes0 ); - cuddDeref( bRes1 ); - - cuddCacheInsert1( dd, extraBddSpaceFromFunctionNeg, bF, bRes ); - return bRes; - } -} - - - -/**Function************************************************************* - - Synopsis [Performs the recursive step of Extra_bddSpaceCanonVars().] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bF ) -{ - DdNode * bRes, * bFR; - statLine( dd ); - - bFR = Cudd_Regular(bF); - if ( cuddIsConstant(bFR) ) - return bF; - - if ( bRes = cuddCacheLookup1(dd, extraBddSpaceCanonVars, bF) ) - return bRes; - else - { - DdNode * bF0, * bF1; - DdNode * bRes, * bRes0; - - if ( bFR != bF ) // bF is complemented - { - bF0 = Cudd_Not( cuddE(bFR) ); - bF1 = Cudd_Not( cuddT(bFR) ); - } - else - { - bF0 = cuddE(bFR); - bF1 = cuddT(bFR); - } - - if ( bF0 == b0 ) - { - bRes = extraBddSpaceCanonVars( dd, bF1 ); - if ( bRes == NULL ) - return NULL; - } - else if ( bF1 == b0 ) - { - bRes = extraBddSpaceCanonVars( dd, bF0 ); - if ( bRes == NULL ) - return NULL; - } - else - { - bRes0 = extraBddSpaceCanonVars( dd, bF0 ); - if ( bRes0 == NULL ) - return NULL; - cuddRef( bRes0 ); - - bRes = cuddUniqueInter( dd, bFR->index, bRes0, b0 ); - if ( bRes == NULL ) - { - Cudd_RecursiveDeref( dd,bRes0 ); - return NULL; - } - cuddDeref( bRes0 ); - } - - cuddCacheInsert1( dd, extraBddSpaceCanonVars, bF, bRes ); - return bRes; - } -} - -/**Function************************************************************* - - Synopsis [Performs the recursive step of Extra_bddSpaceEquationsPos().] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * extraBddSpaceEquationsPos( DdManager * dd, DdNode * bF ) -{ - DdNode * zRes; - statLine( dd ); - - if ( bF == b0 ) - return z1; - if ( bF == b1 ) - return z0; - - if ( zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsPos, bF) ) - return zRes; - else - { - DdNode * bFR, * bF0, * bF1; - DdNode * zPos0, * zPos1, * zNeg1; - DdNode * zRes, * zRes0, * zRes1; - - bFR = Cudd_Regular(bF); - if ( bFR != bF ) // bF is complemented - { - bF0 = Cudd_Not( cuddE(bFR) ); - bF1 = Cudd_Not( cuddT(bFR) ); - } - else - { - bF0 = cuddE(bFR); - bF1 = cuddT(bFR); - } - - if ( bF0 == b0 ) - { - zRes1 = extraBddSpaceEquationsPos( dd, bF1 ); - if ( zRes1 == NULL ) - return NULL; - cuddRef( zRes1 ); - - // add the current element to the set - zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes1 ); - if ( zRes == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zRes1); - return NULL; - } - cuddDeref( zRes1 ); - } - else if ( bF1 == b0 ) - { - zRes = extraBddSpaceEquationsPos( dd, bF0 ); - if ( zRes == NULL ) - return NULL; - } - else - { - zPos0 = extraBddSpaceEquationsPos( dd, bF0 ); - if ( zPos0 == NULL ) - return NULL; - cuddRef( zPos0 ); - - zPos1 = extraBddSpaceEquationsPos( dd, bF1 ); - if ( zPos1 == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zPos0); - return NULL; - } - cuddRef( zPos1 ); - - zNeg1 = extraBddSpaceEquationsNeg( dd, bF1 ); - if ( zNeg1 == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zPos0); - Cudd_RecursiveDerefZdd(dd, zPos1); - return NULL; - } - cuddRef( zNeg1 ); - - - zRes0 = cuddZddIntersect( dd, zPos0, zPos1 ); - if ( zRes0 == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zNeg1); - Cudd_RecursiveDerefZdd(dd, zPos0); - Cudd_RecursiveDerefZdd(dd, zPos1); - return NULL; - } - cuddRef( zRes0 ); - - zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 ); - if ( zRes1 == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zRes0); - Cudd_RecursiveDerefZdd(dd, zNeg1); - Cudd_RecursiveDerefZdd(dd, zPos0); - Cudd_RecursiveDerefZdd(dd, zPos1); - return NULL; - } - cuddRef( zRes1 ); - Cudd_RecursiveDerefZdd(dd, zNeg1); - Cudd_RecursiveDerefZdd(dd, zPos0); - Cudd_RecursiveDerefZdd(dd, zPos1); - // only zRes0 and zRes1 are refed at this point - - zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 ); - if ( zRes == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zRes0); - Cudd_RecursiveDerefZdd(dd, zRes1); - return NULL; - } - cuddDeref( zRes0 ); - cuddDeref( zRes1 ); - } - - cuddCacheInsert1( dd, extraBddSpaceEquationsPos, bF, zRes ); - return zRes; - } -} - - -/**Function************************************************************* - - Synopsis [Performs the recursive step of Extra_bddSpaceEquationsNev().] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bF ) -{ - DdNode * zRes; - statLine( dd ); - - if ( bF == b0 ) - return z1; - if ( bF == b1 ) - return z0; - - if ( zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsNeg, bF) ) - return zRes; - else - { - DdNode * bFR, * bF0, * bF1; - DdNode * zPos0, * zPos1, * zNeg1; - DdNode * zRes, * zRes0, * zRes1; - - bFR = Cudd_Regular(bF); - if ( bFR != bF ) // bF is complemented - { - bF0 = Cudd_Not( cuddE(bFR) ); - bF1 = Cudd_Not( cuddT(bFR) ); - } - else - { - bF0 = cuddE(bFR); - bF1 = cuddT(bFR); - } - - if ( bF0 == b0 ) - { - zRes = extraBddSpaceEquationsNeg( dd, bF1 ); - if ( zRes == NULL ) - return NULL; - } - else if ( bF1 == b0 ) - { - zRes0 = extraBddSpaceEquationsNeg( dd, bF0 ); - if ( zRes0 == NULL ) - return NULL; - cuddRef( zRes0 ); - - // add the current element to the set - zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes0 ); - if ( zRes == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zRes0); - return NULL; - } - cuddDeref( zRes0 ); - } - else - { - zPos0 = extraBddSpaceEquationsNeg( dd, bF0 ); - if ( zPos0 == NULL ) - return NULL; - cuddRef( zPos0 ); - - zPos1 = extraBddSpaceEquationsNeg( dd, bF1 ); - if ( zPos1 == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zPos0); - return NULL; - } - cuddRef( zPos1 ); - - zNeg1 = extraBddSpaceEquationsPos( dd, bF1 ); - if ( zNeg1 == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zPos0); - Cudd_RecursiveDerefZdd(dd, zPos1); - return NULL; - } - cuddRef( zNeg1 ); - - - zRes0 = cuddZddIntersect( dd, zPos0, zPos1 ); - if ( zRes0 == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zNeg1); - Cudd_RecursiveDerefZdd(dd, zPos0); - Cudd_RecursiveDerefZdd(dd, zPos1); - return NULL; - } - cuddRef( zRes0 ); - - zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 ); - if ( zRes1 == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zRes0); - Cudd_RecursiveDerefZdd(dd, zNeg1); - Cudd_RecursiveDerefZdd(dd, zPos0); - Cudd_RecursiveDerefZdd(dd, zPos1); - return NULL; - } - cuddRef( zRes1 ); - Cudd_RecursiveDerefZdd(dd, zNeg1); - Cudd_RecursiveDerefZdd(dd, zPos0); - Cudd_RecursiveDerefZdd(dd, zPos1); - // only zRes0 and zRes1 are refed at this point - - zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 ); - if ( zRes == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zRes0); - Cudd_RecursiveDerefZdd(dd, zRes1); - return NULL; - } - cuddDeref( zRes0 ); - cuddDeref( zRes1 ); - } - - cuddCacheInsert1( dd, extraBddSpaceEquationsNeg, bF, zRes ); - return zRes; - } -} - - - - -/**Function************************************************************* - - Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ) -{ - DdNode * bRes; - statLine( dd ); - - if ( zA == z0 ) - return b1; - if ( zA == z1 ) - return b1; - - if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixPos, zA) ) - return bRes; - else - { - DdNode * bP0, * bP1; - DdNode * bN0, * bN1; - DdNode * bRes0, * bRes1; - - bP0 = extraBddSpaceFromMatrixPos( dd, cuddE(zA) ); - if ( bP0 == NULL ) - return NULL; - cuddRef( bP0 ); - - bP1 = extraBddSpaceFromMatrixPos( dd, cuddT(zA) ); - if ( bP1 == NULL ) - { - Cudd_RecursiveDeref( dd, bP0 ); - return NULL; - } - cuddRef( bP1 ); - - bRes0 = cuddBddAndRecur( dd, bP0, bP1 ); - if ( bRes0 == NULL ) - { - Cudd_RecursiveDeref( dd, bP0 ); - Cudd_RecursiveDeref( dd, bP1 ); - return NULL; - } - cuddRef( bRes0 ); - Cudd_RecursiveDeref( dd, bP0 ); - Cudd_RecursiveDeref( dd, bP1 ); - - - bN0 = extraBddSpaceFromMatrixPos( dd, cuddE(zA) ); - if ( bN0 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - return NULL; - } - cuddRef( bN0 ); - - bN1 = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) ); - if ( bN1 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - Cudd_RecursiveDeref( dd, bN0 ); - return NULL; - } - cuddRef( bN1 ); - - bRes1 = cuddBddAndRecur( dd, bN0, bN1 ); - if ( bRes1 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - Cudd_RecursiveDeref( dd, bN0 ); - Cudd_RecursiveDeref( dd, bN1 ); - return NULL; - } - cuddRef( bRes1 ); - Cudd_RecursiveDeref( dd, bN0 ); - Cudd_RecursiveDeref( dd, bN1 ); - - - // consider the case when Res0 and Res1 are the same node - if ( bRes0 == bRes1 ) - bRes = bRes1; - // consider the case when Res1 is complemented - else if ( Cudd_IsComplement(bRes1) ) - { - bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) ); - if ( bRes == NULL ) - { - Cudd_RecursiveDeref(dd,bRes0); - Cudd_RecursiveDeref(dd,bRes1); - return NULL; - } - bRes = Cudd_Not(bRes); - } - else - { - bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 ); - if ( bRes == NULL ) - { - Cudd_RecursiveDeref(dd,bRes0); - Cudd_RecursiveDeref(dd,bRes1); - return NULL; - } - } - cuddDeref( bRes0 ); - cuddDeref( bRes1 ); - - cuddCacheInsert1( dd, extraBddSpaceFromMatrixPos, zA, bRes ); - return bRes; - } -} - - -/**Function************************************************************* - - Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ) -{ - DdNode * bRes; - statLine( dd ); - - if ( zA == z0 ) - return b1; - if ( zA == z1 ) - return b0; - - if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixNeg, zA) ) - return bRes; - else - { - DdNode * bP0, * bP1; - DdNode * bN0, * bN1; - DdNode * bRes0, * bRes1; - - bP0 = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) ); - if ( bP0 == NULL ) - return NULL; - cuddRef( bP0 ); - - bP1 = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) ); - if ( bP1 == NULL ) - { - Cudd_RecursiveDeref( dd, bP0 ); - return NULL; - } - cuddRef( bP1 ); - - bRes0 = cuddBddAndRecur( dd, bP0, bP1 ); - if ( bRes0 == NULL ) - { - Cudd_RecursiveDeref( dd, bP0 ); - Cudd_RecursiveDeref( dd, bP1 ); - return NULL; - } - cuddRef( bRes0 ); - Cudd_RecursiveDeref( dd, bP0 ); - Cudd_RecursiveDeref( dd, bP1 ); - - - bN0 = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) ); - if ( bN0 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - return NULL; - } - cuddRef( bN0 ); - - bN1 = extraBddSpaceFromMatrixPos( dd, cuddT(zA) ); - if ( bN1 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - Cudd_RecursiveDeref( dd, bN0 ); - return NULL; - } - cuddRef( bN1 ); - - bRes1 = cuddBddAndRecur( dd, bN0, bN1 ); - if ( bRes1 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - Cudd_RecursiveDeref( dd, bN0 ); - Cudd_RecursiveDeref( dd, bN1 ); - return NULL; - } - cuddRef( bRes1 ); - Cudd_RecursiveDeref( dd, bN0 ); - Cudd_RecursiveDeref( dd, bN1 ); - - - // consider the case when Res0 and Res1 are the same node - if ( bRes0 == bRes1 ) - bRes = bRes1; - // consider the case when Res1 is complemented - else if ( Cudd_IsComplement(bRes1) ) - { - bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) ); - if ( bRes == NULL ) - { - Cudd_RecursiveDeref(dd,bRes0); - Cudd_RecursiveDeref(dd,bRes1); - return NULL; - } - bRes = Cudd_Not(bRes); - } - else - { - bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 ); - if ( bRes == NULL ) - { - Cudd_RecursiveDeref(dd,bRes0); - Cudd_RecursiveDeref(dd,bRes1); - return NULL; - } - } - cuddDeref( bRes0 ); - cuddDeref( bRes1 ); - - cuddCacheInsert1( dd, extraBddSpaceFromMatrixNeg, zA, bRes ); - return bRes; - } -} - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - diff --git a/src/misc/extra/extraBddCas.c b/src/misc/extra/extraBddCas.c deleted file mode 100644 index 29382bfb..00000000 --- a/src/misc/extra/extraBddCas.c +++ /dev/null @@ -1,1230 +0,0 @@ -/**CFile**************************************************************** - - FileName [extraBddCas.c] - - PackageName [extra] - - Synopsis [Procedures related to LUT cascade synthesis.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 2.0. Started - September 1, 2003.] - - Revision [$Id: extraBddCas.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $] - -***********************************************************************/ - -#include "extra.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - -// the table to store cofactor operations -#define _TABLESIZE_COF 51113 -typedef struct -{ - unsigned Sign; - DdNode * Arg1; -} _HashEntry_cof; -_HashEntry_cof HHTable1[_TABLESIZE_COF]; - -// the table to store the result of computation of the number of minterms -#define _TABLESIZE_MINT 15113 -typedef struct -{ - DdNode * Arg1; - unsigned Arg2; - unsigned Res; -} _HashEntry_mint; -_HashEntry_mint HHTable2[_TABLESIZE_MINT]; - -typedef struct -{ - int nEdges; // the number of in-coming edges of the node - DdNode * bSum; // the sum of paths of the incoming edges -} traventry; - -// the signature used for hashing -static unsigned s_Signature = 1; - -static int s_CutLevel = 0; - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -// because the proposed solution to the optimal encoding problem has exponential complexity -// we limit the depth of the branch and bound procedure to 5 levels -static int s_MaxDepth = 5; - -static int s_nVarsBest; // the number of vars in the best ordering -static int s_VarOrderBest[32]; // storing the best ordering of vars in the "simple encoding" -static int s_VarOrderCur[32]; // storing the current ordering of vars - -// the place to store the supports of the encoded function -static DdNode * s_Field[8][256]; // the size should be K, 2^K, where K is no less than MaxDepth -static DdNode * s_Encoded; // this is the original function -static DdNode * s_VarAll; // the set of all column variables -static int s_MultiStart; // the total number of encoding variables used -// the array field now stores the supports - -static DdNode ** s_pbTemp; // the temporary storage for the columns - -static int s_BackTracks; -static int s_BackTrackLimit = 100; - -static DdNode * s_Terminal; // the terminal value for counting minterms - - -static int s_EncodingVarsLevel; - - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static DdNode * CreateTheCodes_rec( DdManager * dd, DdNode * bEncoded, int Level, DdNode ** pCVars ); -static void EvaluateEncodings_rec( DdManager * dd, DdNode * bVarsCol, int nVarsCol, int nMulti, int Level ); -// functions called from EvaluateEncodings_rec() -static DdNode * ComputeVarSetAndCountMinterms( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost ); -static DdNode * ComputeVarSetAndCountMinterms2( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost ); -unsigned Extra_CountCofactorMinterms( DdManager * dd, DdNode * bFunc, DdNode * bVarsCof, DdNode * bVarsAll ); -static unsigned Extra_CountMintermsSimple( DdNode * bFunc, unsigned max ); - -static void CountNodeVisits_rec( DdManager * dd, DdNode * aFunc, st_table * Visited ); -static void CollectNodesAndComputePaths_rec( DdManager * dd, DdNode * aFunc, DdNode * bCube, st_table * Visited, st_table * CutNodes ); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Performs the binary encoding of the set of function using the given vars.] - - Description [Performs a straight binary encoding of the set of functions using - the variable cubes formed from the given set of variables. ] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * -Extra_bddEncodingBinary( - DdManager * dd, - DdNode ** pbFuncs, // pbFuncs is the array of columns to be encoded - int nFuncs, // nFuncs is the number of columns in the array - DdNode ** pbVars, // pbVars is the array of variables to use for the codes - int nVars ) // nVars is the column multiplicity, [log2(nFuncs)] -{ - int i; - DdNode * bResult; - DdNode * bCube, * bTemp, * bProd; - - assert( nVars >= Extra_Base2Log(nFuncs) ); - - bResult = b0; Cudd_Ref( bResult ); - for ( i = 0; i < nFuncs; i++ ) - { - bCube = Extra_bddBitsToCube( dd, i, nVars, pbVars, 1 ); Cudd_Ref( bCube ); - bProd = Cudd_bddAnd( dd, bCube, pbFuncs[i] ); Cudd_Ref( bProd ); - Cudd_RecursiveDeref( dd, bCube ); - - bResult = Cudd_bddOr( dd, bProd, bTemp = bResult ); Cudd_Ref( bResult ); - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bProd ); - } - - Cudd_Deref( bResult ); - return bResult; -} /* end of Extra_bddEncodingBinary */ - - -/**Function******************************************************************** - - Synopsis [Solves the column encoding problem using a sophisticated method.] - - Description [The encoding is based on the idea of deriving functions which - depend on only one variable, which corresponds to the case of non-disjoint - decompostion. It is assumed that the variables pCVars are ordered below the variables - representing the solumns, and the first variable pCVars[0] is the topmost one.] - - SideEffects [] - - SeeAlso [Extra_bddEncodingBinary] - -******************************************************************************/ - -DdNode * -Extra_bddEncodingNonStrict( - DdManager * dd, - DdNode ** pbColumns, // pbColumns is the array of columns to be encoded; - int nColumns, // nColumns is the number of columns in the array - DdNode * bVarsCol, // bVarsCol is the cube of variables on which the columns depend - DdNode ** pCVars, // pCVars is the array of variables to use for the codes - int nMulti, // nMulti is the column multiplicity, [log2(nColumns)] - int * pSimple ) // pSimple gets the number of code variables taken from the input varibles without change -{ - DdNode * bEncoded, * bResult; - int nVarsCol = Cudd_SupportSize(dd,bVarsCol); - long clk; - - // cannot work with more that 32-bit codes - assert( nMulti < 32 ); - - // perform the preliminary encoding using the straight binary code - bEncoded = Extra_bddEncodingBinary( dd, pbColumns, nColumns, pCVars, nMulti ); Cudd_Ref( bEncoded ); - //printf( "Node count = %d", Cudd_DagSize(bEncoded) ); - - // set the backgroup value for counting minterms - s_Terminal = b0; - // set the level of the encoding variables - s_EncodingVarsLevel = dd->invperm[pCVars[0]->index]; - - // the current number of backtracks - s_BackTracks = 0; - // the variables that are cofactored on the topmost level where everything starts (no vars) - s_Field[0][0] = b1; - // the size of the best set of "simple" encoding variables found so far - s_nVarsBest = 0; - - // set the relation to be accessible to traversal procedures - s_Encoded = bEncoded; - // the set of all vars to be accessible to traversal procedures - s_VarAll = bVarsCol; - // the column multiplicity - s_MultiStart = nMulti; - - - clk = clock(); - // find the simplest encoding - if ( nColumns > 2 ) - EvaluateEncodings_rec( dd, bVarsCol, nVarsCol, nMulti, 1 ); -// printf( "The number of backtracks = %d\n", s_BackTracks ); -// s_EncSearchTime += clock() - clk; - - // allocate the temporary storage for the columns - s_pbTemp = (DdNode **) malloc( nColumns * sizeof(DdNode *) ); - -// clk = clock(); - bResult = CreateTheCodes_rec( dd, bEncoded, 0, pCVars ); Cudd_Ref( bResult ); -// s_EncComputeTime += clock() - clk; - - // delocate the preliminarily encoded set - Cudd_RecursiveDeref( dd, bEncoded ); -// Cudd_RecursiveDeref( dd, aEncoded ); - - free( s_pbTemp ); - - *pSimple = s_nVarsBest; - Cudd_Deref( bResult ); - return bResult; -} - -/**Function******************************************************************** - - Synopsis [Collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root.] - - Description [The table returned contains the set of BDD nodes pointed to under the cut - and, for each node, the BDD of the sum of paths leading to this node from the root - The sums of paths in the table are referenced. CutLevel is the first DD level - considered to be under the cut.] - - SideEffects [] - - SeeAlso [Extra_bddNodePaths] - -******************************************************************************/ -st_table * Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLevel ) -{ - st_table * Visited; // temporary table to remember the visited nodes - st_table * CutNodes; // the result goes here - st_table * Result; // the result goes here - DdNode * aFunc; - - s_CutLevel = CutLevel; - - Result = st_init_table(st_ptrcmp,st_ptrhash); - // the terminal cases - if ( Cudd_IsConstant( bFunc ) ) - { - if ( bFunc == b1 ) - { - st_insert( Result, (char*)b1, (char*)b1 ); - Cudd_Ref( b1 ); - Cudd_Ref( b1 ); - } - else - { - st_insert( Result, (char*)b0, (char*)b0 ); - Cudd_Ref( b0 ); - Cudd_Ref( b0 ); - } - return Result; - } - - // create the ADD to simplify processing (no complemented edges) - aFunc = Cudd_BddToAdd( dd, bFunc ); Cudd_Ref( aFunc ); - - // Step 1: Start the tables and collect information about the nodes above the cut - // this information tells how many edges point to each node - Visited = st_init_table(st_ptrcmp,st_ptrhash); - CutNodes = st_init_table(st_ptrcmp,st_ptrhash); - - CountNodeVisits_rec( dd, aFunc, Visited ); - - // Step 2: Traverse the BDD using the visited table and compute the sum of paths - CollectNodesAndComputePaths_rec( dd, aFunc, b1, Visited, CutNodes ); - - // at this point the table of cut nodes is ready and the table of visited is useless - { - st_generator * gen; - DdNode * aNode; - traventry * p; - st_foreach_item( Visited, gen, (char**)&aNode, (char**)&p ) - { - Cudd_RecursiveDeref( dd, p->bSum ); - free( p ); - } - st_free_table( Visited ); - } - - // go through the table CutNodes and create the BDD and the path to be returned - { - st_generator * gen; - DdNode * aNode, * bNode, * bSum; - st_foreach_item( CutNodes, gen, (char**)&aNode, (char**)&bSum) - { - // aNode is not referenced, because aFunc is holding it - bNode = Cudd_addBddPattern( dd, aNode ); Cudd_Ref( bNode ); - st_insert( Result, (char*)bNode, (char*)bSum ); - // the new table takes both refs - } - st_free_table( CutNodes ); - } - - // dereference the ADD - Cudd_RecursiveDeref( dd, aFunc ); - - // return the table - return Result; - -} /* end of Extra_bddNodePathsUnderCut */ - -/**Function******************************************************************** - - Synopsis [Collects the nodes under the cut in the ADD starting from the given set of ADD nodes.] - - Description [Takes the array, paNodes, of ADD nodes to start the traversal, - the array, pbCubes, of BDD cubes to start the traversal with in each node, - and the number, nNodes, of ADD nodes and BDD cubes in paNodes and pbCubes. - Returns the number of columns found. Fills in paNodesRes (pbCubesRes) - with the set of ADD columns (BDD paths). These arrays should be allocated - by the user.] - - SideEffects [] - - SeeAlso [Extra_bddNodePaths] - -******************************************************************************/ -int Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode ** pbCubes, int nNodes, DdNode ** paNodesRes, DdNode ** pbCubesRes, int CutLevel ) -{ - st_table * Visited; // temporary table to remember the visited nodes - st_table * CutNodes; // the nodes under the cut go here - int i, Counter; - - s_CutLevel = CutLevel; - - // there should be some nodes - assert( nNodes > 0 ); - if ( nNodes == 1 && Cudd_IsConstant( paNodes[0] ) ) - { - if ( paNodes[0] == a1 ) - { - paNodesRes[0] = a1; Cudd_Ref( a1 ); - pbCubesRes[0] = pbCubes[0]; Cudd_Ref( pbCubes[0] ); - } - else - { - paNodesRes[0] = a0; Cudd_Ref( a0 ); - pbCubesRes[0] = pbCubes[0]; Cudd_Ref( pbCubes[0] ); - } - return 1; - } - - // Step 1: Start the table and collect information about the nodes above the cut - // this information tells how many edges point to each node - CutNodes = st_init_table(st_ptrcmp,st_ptrhash); - Visited = st_init_table(st_ptrcmp,st_ptrhash); - - for ( i = 0; i < nNodes; i++ ) - CountNodeVisits_rec( dd, paNodes[i], Visited ); - - // Step 2: Traverse the BDD using the visited table and compute the sum of paths - for ( i = 0; i < nNodes; i++ ) - CollectNodesAndComputePaths_rec( dd, paNodes[i], pbCubes[i], Visited, CutNodes ); - - // at this point, the table of cut nodes is ready and the table of visited is useless - { - st_generator * gen; - DdNode * aNode; - traventry * p; - st_foreach_item( Visited, gen, (char**)&aNode, (char**)&p ) - { - Cudd_RecursiveDeref( dd, p->bSum ); - free( p ); - } - st_free_table( Visited ); - } - - // go through the table CutNodes and create the BDD and the path to be returned - { - st_generator * gen; - DdNode * aNode, * bSum; - Counter = 0; - st_foreach_item( CutNodes, gen, (char**)&aNode, (char**)&bSum) - { - paNodesRes[Counter] = aNode; Cudd_Ref( aNode ); - pbCubesRes[Counter] = bSum; - Counter++; - } - st_free_table( CutNodes ); - } - - // return the number of cofactors found - return Counter; - -} /* end of Extra_bddNodePathsUnderCutArray */ - -/**Function************************************************************* - - Synopsis [Collects all the BDD nodes into the table.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void extraCollectNodes( DdNode * Func, st_table * tNodes ) -{ - DdNode * FuncR; - FuncR = Cudd_Regular(Func); - if ( st_find_or_add( tNodes, (char*)FuncR, NULL ) ) - return; - if ( cuddIsConstant(FuncR) ) - return; - extraCollectNodes( cuddE(FuncR), tNodes ); - extraCollectNodes( cuddT(FuncR), tNodes ); -} - -/**Function************************************************************* - - Synopsis [Collects all the nodes of one DD into the table.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -st_table * Extra_CollectNodes( DdNode * Func ) -{ - st_table * tNodes; - tNodes = st_init_table( st_ptrcmp, st_ptrhash ); - extraCollectNodes( Func, tNodes ); - return tNodes; -} - -/**Function************************************************************* - - Synopsis [Updates the topmost level from which the given node is referenced.] - - Description [Takes the table which maps each BDD nodes (including the constants) - into the topmost level on which this node counts as a cofactor. Takes the topmost - level, on which this node counts as a cofactor (see Extra_ProfileWidthFast(). - Takes the node, for which the table entry should be updated.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void extraProfileUpdateTopLevel( st_table * tNodeTopRef, int TopLevelNew, DdNode * node ) -{ - int * pTopLevel; - - if ( st_find_or_add( tNodeTopRef, (char*)node, (char***)&pTopLevel ) ) - { // the node is already referenced - // the current top level should be updated if it is larger than the new level - if ( *pTopLevel > TopLevelNew ) - *pTopLevel = TopLevelNew; - } - else - { // the node is not referenced - // its level should be set to the current new level - *pTopLevel = TopLevelNew; - } -} -/**Function************************************************************* - - Synopsis [Fast computation of the BDD profile.] - - Description [The array to store the profile is given by the user and should - contain at least as many entries as there is the maximum of the BDD/ZDD - size of the manager PLUS ONE. - When we say that the widths of the DD on level L is W, we mean the following. - Let us create the cut between the level L-1 and the level L and count the number - of different DD nodes pointed to across the cut. This number is the width W. - From this it follows the on level 0, the width is equal to the number of external - pointers to the considered DDs. If there is only one DD, then the profile on - level 0 is always 1. If this DD is rooted in the topmost variable, then the width - on level 1 is always 2, etc. The width at the level equal to dd->size is the - number of terminal nodes in the DD. (Because we consider the first level #0 - and the last level #dd->size, the profile array should contain dd->size+1 entries.) - ] - - SideEffects [This procedure will not work for BDDs w/ complement edges, only for ADDs and ZDDs] - - SeeAlso [] - -***********************************************************************/ -int Extra_ProfileWidth( DdManager * dd, DdNode * Func, int * pProfile, int CutLevel ) -{ - st_generator * gen; - st_table * tNodeTopRef; // this table stores the top level from which this node is pointed to - st_table * tNodes; - DdNode * node; - DdNode * nodeR; - int LevelStart, Limit; - int i, size; - int WidthMax; - - // start the mapping table - tNodeTopRef = st_init_table(st_ptrcmp,st_ptrhash); - // add the topmost node to the profile - extraProfileUpdateTopLevel( tNodeTopRef, 0, Func ); - - // collect all nodes - tNodes = Extra_CollectNodes( Func ); - // go though all the nodes and set the top level the cofactors are pointed from -// Cudd_ForeachNode( dd, Func, genDD, node ) - st_foreach_item( tNodes, gen, (char**)&node, NULL ) - { -// assert( Cudd_Regular(node) ); // this procedure works only with ADD/ZDD (not BDD w/ compl.edges) - nodeR = Cudd_Regular(node); - if ( cuddIsConstant(nodeR) ) - continue; - // this node is not a constant - consider its cofactors - extraProfileUpdateTopLevel( tNodeTopRef, dd->perm[node->index]+1, cuddE(nodeR) ); - extraProfileUpdateTopLevel( tNodeTopRef, dd->perm[node->index]+1, cuddT(nodeR) ); - } - st_free_table( tNodes ); - - // clean the profile - size = ddMax(dd->size, dd->sizeZ) + 1; - for ( i = 0; i < size; i++ ) - pProfile[i] = 0; - - // create the profile - st_foreach_item( tNodeTopRef, gen, (char**)&node, (char**)&LevelStart ) - { - nodeR = Cudd_Regular(node); - Limit = (cuddIsConstant(nodeR))? dd->size: dd->perm[nodeR->index]; - for ( i = LevelStart; i <= Limit; i++ ) - pProfile[i]++; - } - - if ( CutLevel != -1 && CutLevel != 0 ) - size = CutLevel; - - // get the max width - WidthMax = 0; - for ( i = 0; i < size; i++ ) - if ( WidthMax < pProfile[i] ) - WidthMax = pProfile[i]; - - // deref the table - st_free_table( tNodeTopRef ); - - return WidthMax; -} /* end of Extra_ProfileWidth */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Computes the non-strict codes when evaluation is finished.] - - Description [The information about the best code is stored in s_VarOrderBest, - which has s_nVarsBest entries.] - - SideEffects [None] - -******************************************************************************/ -DdNode * CreateTheCodes_rec( DdManager * dd, DdNode * bEncoded, int Level, DdNode ** pCVars ) -// bEncoded is the preliminarily encoded set of columns -// Level is the current level in the recursion -// pCVars are the variables to be used for encoding -{ - DdNode * bRes; - if ( Level == s_nVarsBest ) - { // the terminal case, when we need to remap the encoded function - // from the preliminary encoded variables to the new ones - st_table * CutNodes; - int nCols; -// double nMints; -/* -#ifdef _DEBUG - - { - DdNode * bTemp; - // make sure that the given number of variables is enough - bTemp = Cudd_bddExistAbstract( dd, bEncoded, s_VarAll ); Cudd_Ref( bTemp ); -// nMints = Cudd_CountMinterm( dd, bTemp, s_MultiStart ); - nMints = Extra_CountMintermsSimple( bTemp, (1<<s_MultiStart) ); - if ( nMints > Extra_Power2( s_MultiStart-Level ) ) - { // the number of minterms is too large to encode the columns - // using the given minimum number of encoding variables - assert( 0 ); - } - Cudd_RecursiveDeref( dd, bTemp ); - } -#endif -*/ - // get the columns to be re-encoded - CutNodes = Extra_bddNodePathsUnderCut( dd, bEncoded, s_EncodingVarsLevel ); - // LUT size is the cut level because because the temporary encoding variables - // are above the functional variables - this is not true!!! - // the temporary variables are below! - - // put the entries from the table into the temporary array - { - st_generator * gen; - DdNode * bColumn, * bCode; - nCols = 0; - st_foreach_item( CutNodes, gen, (char**)&bCode, (char**)&bColumn ) - { - if ( bCode == b0 ) - { // the unused part of the columns - Cudd_RecursiveDeref( dd, bColumn ); - Cudd_RecursiveDeref( dd, bCode ); - continue; - } - else - { - s_pbTemp[ nCols ] = bColumn; // takes ref - Cudd_RecursiveDeref( dd, bCode ); - nCols++; - } - } - st_free_table( CutNodes ); -// assert( nCols == (int)nMints ); - } - - // encode the columns - if ( s_MultiStart-Level == 0 ) // we reached the bottom level of recursion - { - assert( nCols == 1 ); -// assert( (int)nMints == 1 ); - bRes = s_pbTemp[0]; Cudd_Ref( bRes ); - } - else - { - bRes = Extra_bddEncodingBinary( dd, s_pbTemp, nCols, pCVars+Level, s_MultiStart-Level ); Cudd_Ref( bRes ); - } - - // deref the columns - { - int i; - for ( i = 0; i < nCols; i++ ) - Cudd_RecursiveDeref( dd, s_pbTemp[i] ); - } - } - else - { - // cofactor the problem as specified in the best solution - DdNode * bCof0, * bCof1; - DdNode * bRes0, * bRes1; - DdNode * bProd0, * bProd1; - DdNode * bTemp; - DdNode * bVarNext = dd->vars[ s_VarOrderBest[Level] ]; - - bCof0 = Cudd_Cofactor( dd, bEncoded, Cudd_Not( bVarNext ) ); Cudd_Ref( bCof0 ); - bCof1 = Cudd_Cofactor( dd, bEncoded, bVarNext ); Cudd_Ref( bCof1 ); - - // call recursively - bRes0 = CreateTheCodes_rec( dd, bCof0, Level+1, pCVars ); Cudd_Ref( bRes0 ); - bRes1 = CreateTheCodes_rec( dd, bCof1, Level+1, pCVars ); Cudd_Ref( bRes1 ); - - Cudd_RecursiveDeref( dd, bCof0 ); - Cudd_RecursiveDeref( dd, bCof1 ); - - // compose the result using the identity (bVarNext <=> pCVars[Level]) - this is wrong! - // compose the result as follows: x'y'F0 + xyF1 - bProd0 = Cudd_bddAnd( dd, Cudd_Not(bVarNext), Cudd_Not(pCVars[Level]) ); Cudd_Ref( bProd0 ); - bProd1 = Cudd_bddAnd( dd, bVarNext , pCVars[Level] ); Cudd_Ref( bProd1 ); - - bProd0 = Cudd_bddAnd( dd, bTemp = bProd0, bRes0 ); Cudd_Ref( bProd0 ); - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bRes0 ); - - bProd1 = Cudd_bddAnd( dd, bTemp = bProd1, bRes1 ); Cudd_Ref( bProd1 ); - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bRes1 ); - - bRes = Cudd_bddOr( dd, bProd0, bProd1 ); Cudd_Ref( bRes ); - - Cudd_RecursiveDeref( dd, bProd0 ); - Cudd_RecursiveDeref( dd, bProd1 ); - } - Cudd_Deref( bRes ); - return bRes; -} - -/**Function******************************************************************** - - Synopsis [Computes the current set of variables and counts the number of minterms.] - - Description [Old implementation.] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -void EvaluateEncodings_rec( DdManager * dd, DdNode * bVarsCol, int nVarsCol, int nMulti, int Level ) -// bVarsCol is the set of remaining variables -// nVarsCol is the number of remaining variables -// nMulti is the number of encoding variables to be used -// Level is the level of recursion, from which this function is called -// if we successfully finish this procedure, Level also stands for how many encoding variabled we saved -{ - int i, k; - int nEntries = (1<<(Level-1)); // the number of entries in the field of the previous level - DdNode * bVars0, * bVars1; // the cofactors - unsigned nMint0, nMint1; // the number of minterms - DdNode * bTempV; - DdNode * bVarTop; - int fBreak; - - - // there is no need to search above this level - if ( Level > s_MaxDepth ) - return; - - // if there are no variables left, quit the research - if ( bVarsCol == b1 ) - return; - - if ( s_BackTracks > s_BackTrackLimit ) - return; - - s_BackTracks++; - - // otherwise, go through the remaining variables - for ( bTempV = bVarsCol; bTempV != b1; bTempV = cuddT(bTempV) ) - { - // the currently tested variable - bVarTop = dd->vars[bTempV->index]; - - // put it into the array - s_VarOrderCur[Level-1] = bTempV->index; - - // go through the entries and fill them out by cofactoring - fBreak = 0; - for ( i = 0; i < nEntries; i++ ) - { - bVars0 = ComputeVarSetAndCountMinterms( dd, s_Field[Level-1][i], Cudd_Not(bVarTop), &nMint0 ); - Cudd_Ref( bVars0 ); - - if ( nMint0 > Extra_Power2( nMulti-1 ) ) - { - // there is no way to encode - dereference and return - Cudd_RecursiveDeref( dd, bVars0 ); - fBreak = 1; - break; - } - - bVars1 = ComputeVarSetAndCountMinterms( dd, s_Field[Level-1][i], bVarTop, &nMint1 ); - Cudd_Ref( bVars1 ); - - if ( nMint1 > Extra_Power2( nMulti-1 ) ) - { - // there is no way to encode - dereference and return - Cudd_RecursiveDeref( dd, bVars0 ); - Cudd_RecursiveDeref( dd, bVars1 ); - fBreak = 1; - break; - } - - // otherwise, add these two cofactors - s_Field[Level][2*i + 0] = bVars0; // takes ref - s_Field[Level][2*i + 1] = bVars1; // takes ref - } - - if ( !fBreak ) - { - DdNode * bVarsRem; - // if we ended up here, it means that the cofactors w.r.t. variable bVarTop satisfy the condition - // save this situation - if ( s_nVarsBest < Level ) - { - s_nVarsBest = Level; - // copy the variable assignment - for ( k = 0; k < Level; k++ ) - s_VarOrderBest[k] = s_VarOrderCur[k]; - } - - // call recursively - // get the new variable set - if ( nMulti-1 > 0 ) - { - bVarsRem = Cudd_bddExistAbstract( dd, bVarsCol, bVarTop ); Cudd_Ref( bVarsRem ); - EvaluateEncodings_rec( dd, bVarsRem, nVarsCol-1, nMulti-1, Level+1 ); - Cudd_RecursiveDeref( dd, bVarsRem ); - } - } - - // deref the contents of the array - for ( k = 0; k < i; k++ ) - { - Cudd_RecursiveDeref( dd, s_Field[Level][2*k + 0] ); - Cudd_RecursiveDeref( dd, s_Field[Level][2*k + 1] ); - } - - // if the solution is found, there is no need to continue - if ( s_nVarsBest == s_MaxDepth ) - return; - - // if the solution is found, there is no need to continue - if ( s_nVarsBest == s_MultiStart ) - return; - } - // at this point, we have tried all possible directions in the space of variables -} - -/**Function******************************************************************** - - Synopsis [Computes the current set of variables and counts the number of minterms.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * ComputeVarSetAndCountMinterms( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost ) -// takes bVars - the variables cofactored so far (some of them may be in negative polarity) -// bVarTop - the topmost variable w.r.t. which to cofactor (may be in negative polarity) -// returns the cost and the new set of variables (bVars & bVarTop) -{ - DdNode * bVarsRes; - - // get the resulting set of variables - bVarsRes = Cudd_bddAnd( dd, bVars, bVarTop ); Cudd_Ref( bVarsRes ); - - // increment signature before calling Cudd_CountCofactorMinterms() - s_Signature++; - *Cost = Extra_CountCofactorMinterms( dd, s_Encoded, bVarsRes, s_VarAll ); - - Cudd_Deref( bVarsRes ); -// s_CountCalls++; - return bVarsRes; -} - -/**Function******************************************************************** - - Synopsis [Computes the current set of variables and counts the number of minterms.] - - Description [The old implementation, which is approximately 4 times slower.] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * ComputeVarSetAndCountMinterms2( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost ) -{ - DdNode * bVarsRes; - DdNode * bCof, * bFun; - - bVarsRes = Cudd_bddAnd( dd, bVars, bVarTop ); Cudd_Ref( bVarsRes ); - - bCof = Cudd_Cofactor( dd, s_Encoded, bVarsRes ); Cudd_Ref( bCof ); - bFun = Cudd_bddExistAbstract( dd, bCof, s_VarAll ); Cudd_Ref( bFun ); - *Cost = (unsigned)Cudd_CountMinterm( dd, bFun, s_MultiStart ); - Cudd_RecursiveDeref( dd, bFun ); - Cudd_RecursiveDeref( dd, bCof ); - - Cudd_Deref( bVarsRes ); -// s_CountCalls++; - return bVarsRes; -} - - -/**Function******************************************************************** - - Synopsis [Counts the number of encoding minterms pointed to by the cofactor of the function.] - - Description [] - - SideEffects [None] - -******************************************************************************/ -unsigned Extra_CountCofactorMinterms( DdManager * dd, DdNode * bFunc, DdNode * bVarsCof, DdNode * bVarsAll ) -// this function computes how many minterms depending on the encoding variables -// are there in the cofactor of bFunc w.r.t. variables bVarsCof -// bFunc is assumed to depend on variables s_VarsAll -// the variables s_VarsAll should be ordered above the encoding variables -{ - unsigned HKey; - DdNode * bFuncR; - - // if the function is zero, there are no minterms -// if ( bFunc == b0 ) -// return 0; - -// if ( st_lookup(Visited, (char*)bFunc, NULL) ) -// return 0; - -// HKey = hashKey2c( s_Signature, bFuncR ); -// if ( HHTable1[HKey].Sign == s_Signature && HHTable1[HKey].Arg1 == bFuncR ) // this node is visited -// return 0; - - - // check the hash-table - bFuncR = Cudd_Regular(bFunc); -// HKey = hashKey2( s_Signature, bFuncR, _TABLESIZE_COF ); - HKey = hashKey2( s_Signature, bFunc, _TABLESIZE_COF ); - for ( ; HHTable1[HKey].Sign == s_Signature; HKey = (HKey+1) % _TABLESIZE_COF ) -// if ( HHTable1[HKey].Arg1 == bFuncR ) // this node is visited - if ( HHTable1[HKey].Arg1 == bFunc ) // this node is visited - return 0; - - - // if the function is already the code - if ( dd->perm[bFuncR->index] >= s_EncodingVarsLevel ) - { -// st_insert(Visited, (char*)bFunc, NULL); - -// HHTable1[HKey].Sign = s_Signature; -// HHTable1[HKey].Arg1 = bFuncR; - - assert( HHTable1[HKey].Sign != s_Signature ); - HHTable1[HKey].Sign = s_Signature; -// HHTable1[HKey].Arg1 = bFuncR; - HHTable1[HKey].Arg1 = bFunc; - - return Extra_CountMintermsSimple( bFunc, (1<<s_MultiStart) ); - } - else - { - DdNode * bFunc0, * bFunc1; - DdNode * bVarsCof0, * bVarsCof1; - DdNode * bVarsCofR = Cudd_Regular(bVarsCof); - unsigned Res; - - // get the levels - int LevelF = dd->perm[bFuncR->index]; - int LevelC = cuddI(dd,bVarsCofR->index); - int LevelA = dd->perm[bVarsAll->index]; - - int LevelTop = LevelF; - - if ( LevelTop > LevelC ) - LevelTop = LevelC; - - if ( LevelTop > LevelA ) - LevelTop = LevelA; - - // the top var in the function or in cofactoring vars always belongs to the set of all vars - assert( !( LevelTop == LevelF || LevelTop == LevelC ) || LevelTop == LevelA ); - - // cofactor the function - if ( LevelTop == LevelF ) - { - if ( bFuncR != bFunc ) // bFunc is complemented - { - bFunc0 = Cudd_Not( cuddE(bFuncR) ); - bFunc1 = Cudd_Not( cuddT(bFuncR) ); - } - else - { - bFunc0 = cuddE(bFuncR); - bFunc1 = cuddT(bFuncR); - } - } - else // bVars is higher in the variable order - bFunc0 = bFunc1 = bFunc; - - // cofactor the cube - if ( LevelTop == LevelC ) - { - if ( bVarsCofR != bVarsCof ) // bFunc is complemented - { - bVarsCof0 = Cudd_Not( cuddE(bVarsCofR) ); - bVarsCof1 = Cudd_Not( cuddT(bVarsCofR) ); - } - else - { - bVarsCof0 = cuddE(bVarsCofR); - bVarsCof1 = cuddT(bVarsCofR); - } - } - else // bVars is higher in the variable order - bVarsCof0 = bVarsCof1 = bVarsCof; - - // there are two cases: - // (1) the top variable belongs to the cofactoring variables - // (2) the top variable does not belong to the cofactoring variables - - // (1) the top variable belongs to the cofactoring variables - Res = 0; - if ( LevelTop == LevelC ) - { - if ( bVarsCof1 == b0 ) // this is a negative cofactor - { - if ( bFunc0 != b0 ) - Res = Extra_CountCofactorMinterms( dd, bFunc0, bVarsCof0, cuddT(bVarsAll) ); - } - else // this is a positive cofactor - { - if ( bFunc1 != b0 ) - Res = Extra_CountCofactorMinterms( dd, bFunc1, bVarsCof1, cuddT(bVarsAll) ); - } - } - else - { - if ( bFunc0 != b0 ) - Res += Extra_CountCofactorMinterms( dd, bFunc0, bVarsCof0, cuddT(bVarsAll) ); - - if ( bFunc1 != b0 ) - Res += Extra_CountCofactorMinterms( dd, bFunc1, bVarsCof1, cuddT(bVarsAll) ); - } - -// st_insert(Visited, (char*)bFunc, NULL); - -// HHTable1[HKey].Sign = s_Signature; -// HHTable1[HKey].Arg1 = bFuncR; - - // skip through the entries with the same signatures - // (these might have been created at the time of recursive calls) - for ( ; HHTable1[HKey].Sign == s_Signature; HKey = (HKey+1) % _TABLESIZE_COF ); - assert( HHTable1[HKey].Sign != s_Signature ); - HHTable1[HKey].Sign = s_Signature; -// HHTable1[HKey].Arg1 = bFuncR; - HHTable1[HKey].Arg1 = bFunc; - - return Res; - } -} - -/**Function******************************************************************** - - Synopsis [Counts the number of minterms.] - - Description [This function counts minterms for functions up to 32 variables - using a local cache. The terminal value (s_Termina) should be adjusted for - BDDs and ADDs.] - - SideEffects [None] - -******************************************************************************/ -unsigned Extra_CountMintermsSimple( DdNode * bFunc, unsigned max ) -{ - unsigned HKey; - - // normalize - if ( Cudd_IsComplement(bFunc) ) - return max - Extra_CountMintermsSimple( Cudd_Not(bFunc), max ); - - // now it is known that the function is not complemented - if ( cuddIsConstant(bFunc) ) - return ((bFunc==s_Terminal)? 0: max); - - // check cache - HKey = hashKey2( bFunc, max, _TABLESIZE_MINT ); - if ( HHTable2[HKey].Arg1 == bFunc && HHTable2[HKey].Arg2 == max ) - return HHTable2[HKey].Res; - else - { - // min = min0/2 + min1/2; - unsigned min = (Extra_CountMintermsSimple( cuddE(bFunc), max ) >> 1) + - (Extra_CountMintermsSimple( cuddT(bFunc), max ) >> 1); - - HHTable2[HKey].Arg1 = bFunc; - HHTable2[HKey].Arg2 = max; - HHTable2[HKey].Res = min; - - return min; - } -} /* end of Extra_CountMintermsSimple */ - - -/**Function******************************************************************** - - Synopsis [Visits the nodes.] - - Description [Visits the nodes above the cut and the nodes pointed to below the cut; - collects the visited nodes, counts how many times each node is visited, and sets - the path-sum to be the constant zero BDD.] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -void CountNodeVisits_rec( DdManager * dd, DdNode * aFunc, st_table * Visited ) - -{ - traventry * p; - char **slot; - if ( st_find_or_add(Visited, (char*)aFunc, &slot) ) - { // the entry already exists - p = (traventry*) *slot; - // increment the counter of incoming edges - p->nEdges++; - return; - } - // this node has not been visited - assert( !Cudd_IsComplement(aFunc) ); - - // create the new traversal entry - p = (traventry *) malloc( sizeof(traventry) ); - // set the initial sum of edges to zero BDD - p->bSum = b0; Cudd_Ref( b0 ); - // set the starting number of incoming edges - p->nEdges = 1; - // set this entry into the slot - *slot = (char*)p; - - // recur if the node is above the cut - if ( cuddI(dd,aFunc->index) < s_CutLevel ) - { - CountNodeVisits_rec( dd, cuddE(aFunc), Visited ); - CountNodeVisits_rec( dd, cuddT(aFunc), Visited ); - } -} /* end of CountNodeVisits_rec */ - - -/**Function******************************************************************** - - Synopsis [Revisits the nodes and computes the paths.] - - Description [This function visits the nodes above the cut having the goal of - summing all the incomming BDD edges; when this function comes across the node - below the cut, it saves this node in the CutNode table.] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -void CollectNodesAndComputePaths_rec( DdManager * dd, DdNode * aFunc, DdNode * bCube, st_table * Visited, st_table * CutNodes ) -{ - // find the node in the visited table - DdNode * bTemp; - traventry * p; - char **slot; - if ( st_find_or_add(Visited, (char*)aFunc, &slot) ) - { // the node is found - // get the pointer to the traversal entry - p = (traventry*) *slot; - - // make sure that the counter of incoming edges is positive - assert( p->nEdges > 0 ); - - // add the cube to the currently accumulated cubes - p->bSum = Cudd_bddOr( dd, bTemp = p->bSum, bCube ); Cudd_Ref( p->bSum ); - Cudd_RecursiveDeref( dd, bTemp ); - - // decrement the number of visits - p->nEdges--; - - // if more visits to this node are expected, return - if ( p->nEdges ) - return; - else // if ( p->nEdges == 0 ) - { // this is the last visit - propagate the cube - - // check where this node is - if ( cuddI(dd,aFunc->index) < s_CutLevel ) - { // the node is above the cut - DdNode * bCube0, * bCube1; - - // get the top-most variable - DdNode * bVarTop = dd->vars[aFunc->index]; - - // compute the propagated cubes - bCube0 = Cudd_bddAnd( dd, p->bSum, Cudd_Not( bVarTop ) ); Cudd_Ref( bCube0 ); - bCube1 = Cudd_bddAnd( dd, p->bSum, bVarTop ); Cudd_Ref( bCube1 ); - - // call recursively - CollectNodesAndComputePaths_rec( dd, cuddE(aFunc), bCube0, Visited, CutNodes ); - CollectNodesAndComputePaths_rec( dd, cuddT(aFunc), bCube1, Visited, CutNodes ); - - // dereference the cubes - Cudd_RecursiveDeref( dd, bCube0 ); - Cudd_RecursiveDeref( dd, bCube1 ); - return; - } - else - { // the node is below the cut - // add this node to the cut node table, if it is not yet there - -// DdNode * bNode; -// bNode = Cudd_addBddPattern( dd, aFunc ); Cudd_Ref( bNode ); - if ( st_find_or_add(CutNodes, (char*)aFunc, &slot) ) - { // the node exists - should never happen - assert( 0 ); - } - *slot = (char*) p->bSum; Cudd_Ref( p->bSum ); - // the table takes the reference of bNode - return; - } - } - } - - // the node does not exist in the visited table - should never happen - assert(0); - -} /* end of CollectNodesAndComputePaths_rec */ - - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// diff --git a/src/misc/extra/extraBddKmap.c b/src/misc/extra/extraBddKmap.c deleted file mode 100644 index bb43db68..00000000 --- a/src/misc/extra/extraBddKmap.c +++ /dev/null @@ -1,783 +0,0 @@ -/**CFile**************************************************************** - - FileName [extraBddKmap.c] - - PackageName [extra] - - Synopsis [Visualizing the K-map.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 2.0. Started - September 1, 2003.] - - Revision [$Id: extraBddKmap.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $] - -***********************************************************************/ - -/// K-map visualization using pseudo graphics /// -/// Version 1.0. Started - August 20, 2000 /// -/// Version 2.0. Added to EXTRA - July 17, 2001 /// - -#include "extra.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - -// the maximum number of variables in the Karnaugh Map -#define MAXVARS 20 - -/* -// single line -#define SINGLE_VERTICAL (char)179 -#define SINGLE_HORIZONTAL (char)196 -#define SINGLE_TOP_LEFT (char)218 -#define SINGLE_TOP_RIGHT (char)191 -#define SINGLE_BOT_LEFT (char)192 -#define SINGLE_BOT_RIGHT (char)217 - -// double line -#define DOUBLE_VERTICAL (char)186 -#define DOUBLE_HORIZONTAL (char)205 -#define DOUBLE_TOP_LEFT (char)201 -#define DOUBLE_TOP_RIGHT (char)187 -#define DOUBLE_BOT_LEFT (char)200 -#define DOUBLE_BOT_RIGHT (char)188 - -// line intersections -#define SINGLES_CROSS (char)197 -#define DOUBLES_CROSS (char)206 -#define S_HOR_CROSS_D_VER (char)215 -#define S_VER_CROSS_D_HOR (char)216 - -// single line joining -#define S_JOINS_S_VER_LEFT (char)180 -#define S_JOINS_S_VER_RIGHT (char)195 -#define S_JOINS_S_HOR_TOP (char)193 -#define S_JOINS_S_HOR_BOT (char)194 - -// double line joining -#define D_JOINS_D_VER_LEFT (char)185 -#define D_JOINS_D_VER_RIGHT (char)204 -#define D_JOINS_D_HOR_TOP (char)202 -#define D_JOINS_D_HOR_BOT (char)203 - -// single line joining double line -#define S_JOINS_D_VER_LEFT (char)182 -#define S_JOINS_D_VER_RIGHT (char)199 -#define S_JOINS_D_HOR_TOP (char)207 -#define S_JOINS_D_HOR_BOT (char)209 -*/ - -// single line -#define SINGLE_VERTICAL (char)'|' -#define SINGLE_HORIZONTAL (char)'-' -#define SINGLE_TOP_LEFT (char)'+' -#define SINGLE_TOP_RIGHT (char)'+' -#define SINGLE_BOT_LEFT (char)'+' -#define SINGLE_BOT_RIGHT (char)'+' - -// double line -#define DOUBLE_VERTICAL (char)'|' -#define DOUBLE_HORIZONTAL (char)'-' -#define DOUBLE_TOP_LEFT (char)'+' -#define DOUBLE_TOP_RIGHT (char)'+' -#define DOUBLE_BOT_LEFT (char)'+' -#define DOUBLE_BOT_RIGHT (char)'+' - -// line intersections -#define SINGLES_CROSS (char)'+' -#define DOUBLES_CROSS (char)'+' -#define S_HOR_CROSS_D_VER (char)'+' -#define S_VER_CROSS_D_HOR (char)'+' - -// single line joining -#define S_JOINS_S_VER_LEFT (char)'+' -#define S_JOINS_S_VER_RIGHT (char)'+' -#define S_JOINS_S_HOR_TOP (char)'+' -#define S_JOINS_S_HOR_BOT (char)'+' - -// double line joining -#define D_JOINS_D_VER_LEFT (char)'+' -#define D_JOINS_D_VER_RIGHT (char)'+' -#define D_JOINS_D_HOR_TOP (char)'+' -#define D_JOINS_D_HOR_BOT (char)'+' - -// single line joining double line -#define S_JOINS_D_VER_LEFT (char)'+' -#define S_JOINS_D_VER_RIGHT (char)'+' -#define S_JOINS_D_HOR_TOP (char)'+' -#define S_JOINS_D_HOR_BOT (char)'+' - - -// other symbols -#define UNDERSCORE (char)95 -//#define SYMBOL_ZERO (char)248 // degree sign -//#define SYMBOL_ZERO (char)'o' -#define SYMBOL_ZERO (char)' ' -#define SYMBOL_ONE (char)'1' -#define SYMBOL_DC (char)'-' -#define SYMBOL_OVERLAP (char)'?' - -// full cells and half cells -#define CELL_FREE (char)32 -#define CELL_FULL (char)219 -#define HALF_UPPER (char)223 -#define HALF_LOWER (char)220 -#define HALF_LEFT (char)221 -#define HALF_RIGHT (char)222 - - -/*---------------------------------------------------------------------------*/ -/* Structure declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -// the array of BDD variables used internally -static DdNode * s_XVars[MAXVARS]; - -// flag which determines where the horizontal variable names are printed -static int fHorizontalVarNamesPrintedAbove = 1; - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -// Oleg's way of generating the gray code -static int GrayCode( int BinCode ); -static int BinCode ( int GrayCode ); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Prints the K-map of the function.] - - Description [If the pointer to the array of variables XVars is NULL, - fSuppType determines how the support will be determined. - fSuppType == 0 -- takes the first nVars of the manager - fSuppType == 1 -- takes the topmost nVars of the manager - fSuppType == 2 -- determines support from the on-set and the offset - ] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -void Extra_PrintKMap( - FILE * Output, /* the output stream */ - DdManager * dd, - DdNode * OnSet, - DdNode * OffSet, - int nVars, - DdNode ** XVars, - int fSuppType, /* the flag which determines how support is computed */ - char ** pVarNames ) -{ - int d, p, n, s, v, h, w; - int nVarsVer; - int nVarsHor; - int nCellsVer; - int nCellsHor; - int nSkipSpaces; - - // make sure that on-set and off-set do not overlap - if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) ) - { - fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" ); - return; - } -/* - if ( OnSet == b1 ) - { - fprintf( Output, "PrintKMap(): Constant 1\n" ); - return; - } - if ( OffSet == b1 ) - { - fprintf( Output, "PrintKMap(): Constant 0\n" ); - return; - } -*/ - if ( nVars < 0 || nVars > MAXVARS ) - { - fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS ); - return; - } - - // determine the support if it is not given - if ( XVars == NULL ) - { - if ( fSuppType == 0 ) - { // assume that the support includes the first nVars of the manager - assert( nVars ); - for ( v = 0; v < nVars; v++ ) - s_XVars[v] = Cudd_bddIthVar( dd, v ); - } - else if ( fSuppType == 1 ) - { // assume that the support includes the topmost nVars of the manager - assert( nVars ); - for ( v = 0; v < nVars; v++ ) - s_XVars[v] = Cudd_bddIthVar( dd, dd->invperm[v] ); - } - else // determine the support - { - DdNode * SuppOn, * SuppOff, * Supp; - int cVars = 0; - DdNode * TempSupp; - - // determine support - SuppOn = Cudd_Support( dd, OnSet ); Cudd_Ref( SuppOn ); - SuppOff = Cudd_Support( dd, OffSet ); Cudd_Ref( SuppOff ); - Supp = Cudd_bddAnd( dd, SuppOn, SuppOff ); Cudd_Ref( Supp ); - Cudd_RecursiveDeref( dd, SuppOn ); - Cudd_RecursiveDeref( dd, SuppOff ); - - nVars = Cudd_SupportSize( dd, Supp ); - if ( nVars > MAXVARS ) - { - fprintf( Output, "PrintKMap(): The number of variables is more than %d\n", MAXVARS ); - Cudd_RecursiveDeref( dd, Supp ); - return; - } - - // assign variables - for ( TempSupp = Supp; TempSupp != dd->one; TempSupp = Cudd_T(TempSupp), cVars++ ) - s_XVars[cVars] = Cudd_bddIthVar( dd, TempSupp->index ); - - Cudd_RecursiveDeref( dd, TempSupp ); - } - } - else - { - // copy variables - assert( XVars ); - for ( v = 0; v < nVars; v++ ) - s_XVars[v] = XVars[v]; - } - - //////////////////////////////////////////////////////////////////// - // determine the Karnaugh map parameters - nVarsVer = nVars/2; - nVarsHor = nVars - nVarsVer; - nCellsVer = (1<<nVarsVer); - nCellsHor = (1<<nVarsHor); - nSkipSpaces = nVarsVer + 1; - - //////////////////////////////////////////////////////////////////// - // print variable names - fprintf( Output, "\n" ); - for ( w = 0; w < nVarsVer; w++ ) - if ( pVarNames == NULL ) - fprintf( Output, "%c", 'a'+nVarsHor+w ); - else - fprintf( Output, " %s", pVarNames[nVarsHor+w] ); - - if ( fHorizontalVarNamesPrintedAbove ) - { - fprintf( Output, " \\ " ); - for ( w = 0; w < nVarsHor; w++ ) - if ( pVarNames == NULL ) - fprintf( Output, "%c", 'a'+w ); - else - fprintf( Output, "%s ", pVarNames[w] ); - } - fprintf( Output, "\n" ); - - if ( fHorizontalVarNamesPrintedAbove ) - { - //////////////////////////////////////////////////////////////////// - // print horizontal digits - for ( d = 0; d < nVarsHor; d++ ) - { - for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) ); - for ( n = 0; n < nCellsHor; n++ ) - if ( GrayCode(n) & (1<<(nVarsHor-1-d)) ) - fprintf( Output, "1 " ); - else - fprintf( Output, "0 " ); - fprintf( Output, "\n" ); - } - } - - //////////////////////////////////////////////////////////////////// - // print the upper line - for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); - fprintf( Output, "%c", DOUBLE_TOP_LEFT ); - for ( s = 0; s < nCellsHor; s++ ) - { - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - if ( s != nCellsHor-1 ) - if ( s&1 ) - fprintf( Output, "%c", D_JOINS_D_HOR_BOT ); - else - fprintf( Output, "%c", S_JOINS_D_HOR_BOT ); - } - fprintf( Output, "%c", DOUBLE_TOP_RIGHT ); - fprintf( Output, "\n" ); - - //////////////////////////////////////////////////////////////////// - // print the map - for ( v = 0; v < nCellsVer; v++ ) - { - DdNode * CubeVerBDD; - - // print horizontal digits -// for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); - for ( n = 0; n < nVarsVer; n++ ) - if ( GrayCode(v) & (1<<(nVarsVer-1-n)) ) - fprintf( Output, "1" ); - else - fprintf( Output, "0" ); - fprintf( Output, " " ); - - // find vertical cube - CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nVarsVer, s_XVars+nVarsHor, 1 ); Cudd_Ref( CubeVerBDD ); - - // print text line - fprintf( Output, "%c", DOUBLE_VERTICAL ); - for ( h = 0; h < nCellsHor; h++ ) - { - DdNode * CubeHorBDD, * Prod, * ValueOnSet, * ValueOffSet; - - fprintf( Output, " " ); -// fprintf( Output, "x" ); - /////////////////////////////////////////////////////////////// - // determine what should be printed - CubeHorBDD = Extra_bddBitsToCube( dd, GrayCode(h), nVarsHor, s_XVars, 1 ); Cudd_Ref( CubeHorBDD ); - Prod = Cudd_bddAnd( dd, CubeHorBDD, CubeVerBDD ); Cudd_Ref( Prod ); - Cudd_RecursiveDeref( dd, CubeHorBDD ); - - ValueOnSet = Cudd_Cofactor( dd, OnSet, Prod ); Cudd_Ref( ValueOnSet ); - ValueOffSet = Cudd_Cofactor( dd, OffSet, Prod ); Cudd_Ref( ValueOffSet ); - Cudd_RecursiveDeref( dd, Prod ); - - if ( ValueOnSet == b1 && ValueOffSet == b0 ) - fprintf( Output, "%c", SYMBOL_ONE ); - else if ( ValueOnSet == b0 && ValueOffSet == b1 ) - fprintf( Output, "%c", SYMBOL_ZERO ); - else if ( ValueOnSet == b0 && ValueOffSet == b0 ) - fprintf( Output, "%c", SYMBOL_DC ); - else if ( ValueOnSet == b1 && ValueOffSet == b1 ) - fprintf( Output, "%c", SYMBOL_OVERLAP ); - else - assert(0); - - Cudd_RecursiveDeref( dd, ValueOnSet ); - Cudd_RecursiveDeref( dd, ValueOffSet ); - /////////////////////////////////////////////////////////////// - fprintf( Output, " " ); - - if ( h != nCellsHor-1 ) - if ( h&1 ) - fprintf( Output, "%c", DOUBLE_VERTICAL ); - else - fprintf( Output, "%c", SINGLE_VERTICAL ); - } - fprintf( Output, "%c", DOUBLE_VERTICAL ); - fprintf( Output, "\n" ); - - Cudd_RecursiveDeref( dd, CubeVerBDD ); - - if ( v != nCellsVer-1 ) - // print separator line - { - for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); - if ( v&1 ) - { - fprintf( Output, "%c", D_JOINS_D_VER_RIGHT ); - for ( s = 0; s < nCellsHor; s++ ) - { - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - if ( s != nCellsHor-1 ) - if ( s&1 ) - fprintf( Output, "%c", DOUBLES_CROSS ); - else - fprintf( Output, "%c", S_VER_CROSS_D_HOR ); - } - fprintf( Output, "%c", D_JOINS_D_VER_LEFT ); - } - else - { - fprintf( Output, "%c", S_JOINS_D_VER_RIGHT ); - for ( s = 0; s < nCellsHor; s++ ) - { - fprintf( Output, "%c", SINGLE_HORIZONTAL ); - fprintf( Output, "%c", SINGLE_HORIZONTAL ); - fprintf( Output, "%c", SINGLE_HORIZONTAL ); - if ( s != nCellsHor-1 ) - if ( s&1 ) - fprintf( Output, "%c", S_HOR_CROSS_D_VER ); - else - fprintf( Output, "%c", SINGLES_CROSS ); - } - fprintf( Output, "%c", S_JOINS_D_VER_LEFT ); - } - fprintf( Output, "\n" ); - } - } - - //////////////////////////////////////////////////////////////////// - // print the lower line - for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); - fprintf( Output, "%c", DOUBLE_BOT_LEFT ); - for ( s = 0; s < nCellsHor; s++ ) - { - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - if ( s != nCellsHor-1 ) - if ( s&1 ) - fprintf( Output, "%c", D_JOINS_D_HOR_TOP ); - else - fprintf( Output, "%c", S_JOINS_D_HOR_TOP ); - } - fprintf( Output, "%c", DOUBLE_BOT_RIGHT ); - fprintf( Output, "\n" ); - - if ( !fHorizontalVarNamesPrintedAbove ) - { - //////////////////////////////////////////////////////////////////// - // print horizontal digits - for ( d = 0; d < nVarsHor; d++ ) - { - for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) ); - for ( n = 0; n < nCellsHor; n++ ) - if ( GrayCode(n) & (1<<(nVarsHor-1-d)) ) - fprintf( Output, "1 " ); - else - fprintf( Output, "0 " ); - - ///////////////////////////////// - fprintf( Output, "%c", (char)('a'+d) ); - ///////////////////////////////// - fprintf( Output, "\n" ); - } - } -} - - - -/**Function******************************************************************** - - Synopsis [Prints the K-map of the relation.] - - Description [Assumes that the relation depends the first nXVars of XVars and - the first nYVars of YVars. Draws X and Y vars and vertical and horizontal vars.] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -void Extra_PrintKMapRelation( - FILE * Output, /* the output stream */ - DdManager * dd, - DdNode * OnSet, - DdNode * OffSet, - int nXVars, - int nYVars, - DdNode ** XVars, - DdNode ** YVars ) /* the flag which determines how support is computed */ -{ - int d, p, n, s, v, h, w; - int nVars; - int nVarsVer; - int nVarsHor; - int nCellsVer; - int nCellsHor; - int nSkipSpaces; - - // make sure that on-set and off-set do not overlap - if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) ) - { - fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" ); - return; - } - - if ( OnSet == b1 ) - { - fprintf( Output, "PrintKMap(): Constant 1\n" ); - return; - } - if ( OffSet == b1 ) - { - fprintf( Output, "PrintKMap(): Constant 0\n" ); - return; - } - - nVars = nXVars + nYVars; - if ( nVars < 0 || nVars > MAXVARS ) - { - fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS ); - return; - } - - - //////////////////////////////////////////////////////////////////// - // determine the Karnaugh map parameters - nVarsVer = nXVars; - nVarsHor = nYVars; - nCellsVer = (1<<nVarsVer); - nCellsHor = (1<<nVarsHor); - nSkipSpaces = nVarsVer + 1; - - //////////////////////////////////////////////////////////////////// - // print variable names - fprintf( Output, "\n" ); - for ( w = 0; w < nVarsVer; w++ ) - fprintf( Output, "%c", 'a'+nVarsHor+w ); - if ( fHorizontalVarNamesPrintedAbove ) - { - fprintf( Output, " \\ " ); - for ( w = 0; w < nVarsHor; w++ ) - fprintf( Output, "%c", 'a'+w ); - } - fprintf( Output, "\n" ); - - if ( fHorizontalVarNamesPrintedAbove ) - { - //////////////////////////////////////////////////////////////////// - // print horizontal digits - for ( d = 0; d < nVarsHor; d++ ) - { - for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) ); - for ( n = 0; n < nCellsHor; n++ ) - if ( GrayCode(n) & (1<<(nVarsHor-1-d)) ) - fprintf( Output, "1 " ); - else - fprintf( Output, "0 " ); - fprintf( Output, "\n" ); - } - } - - //////////////////////////////////////////////////////////////////// - // print the upper line - for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); - fprintf( Output, "%c", DOUBLE_TOP_LEFT ); - for ( s = 0; s < nCellsHor; s++ ) - { - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - if ( s != nCellsHor-1 ) - if ( s&1 ) - fprintf( Output, "%c", D_JOINS_D_HOR_BOT ); - else - fprintf( Output, "%c", S_JOINS_D_HOR_BOT ); - } - fprintf( Output, "%c", DOUBLE_TOP_RIGHT ); - fprintf( Output, "\n" ); - - //////////////////////////////////////////////////////////////////// - // print the map - for ( v = 0; v < nCellsVer; v++ ) - { - DdNode * CubeVerBDD; - - // print horizontal digits -// for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); - for ( n = 0; n < nVarsVer; n++ ) - if ( GrayCode(v) & (1<<(nVarsVer-1-n)) ) - fprintf( Output, "1" ); - else - fprintf( Output, "0" ); - fprintf( Output, " " ); - - // find vertical cube -// CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nVarsVer, s_XVars+nVarsHor ); Cudd_Ref( CubeVerBDD ); - CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nXVars, XVars, 1 ); Cudd_Ref( CubeVerBDD ); - - // print text line - fprintf( Output, "%c", DOUBLE_VERTICAL ); - for ( h = 0; h < nCellsHor; h++ ) - { - DdNode * CubeHorBDD, * Prod, * ValueOnSet, * ValueOffSet; - - fprintf( Output, " " ); -// fprintf( Output, "x" ); - /////////////////////////////////////////////////////////////// - // determine what should be printed -// CubeHorBDD = Extra_bddBitsToCube( dd, GrayCode(h), nVarsHor, s_XVars ); Cudd_Ref( CubeHorBDD ); - CubeHorBDD = Extra_bddBitsToCube( dd, GrayCode(h), nYVars, YVars, 1 ); Cudd_Ref( CubeHorBDD ); - Prod = Cudd_bddAnd( dd, CubeHorBDD, CubeVerBDD ); Cudd_Ref( Prod ); - Cudd_RecursiveDeref( dd, CubeHorBDD ); - - ValueOnSet = Cudd_Cofactor( dd, OnSet, Prod ); Cudd_Ref( ValueOnSet ); - ValueOffSet = Cudd_Cofactor( dd, OffSet, Prod ); Cudd_Ref( ValueOffSet ); - Cudd_RecursiveDeref( dd, Prod ); - - if ( ValueOnSet == b1 && ValueOffSet == b0 ) - fprintf( Output, "%c", SYMBOL_ONE ); - else if ( ValueOnSet == b0 && ValueOffSet == b1 ) - fprintf( Output, "%c", SYMBOL_ZERO ); - else if ( ValueOnSet == b0 && ValueOffSet == b0 ) - fprintf( Output, "%c", SYMBOL_DC ); - else if ( ValueOnSet == b1 && ValueOffSet == b1 ) - fprintf( Output, "%c", SYMBOL_OVERLAP ); - else - assert(0); - - Cudd_RecursiveDeref( dd, ValueOnSet ); - Cudd_RecursiveDeref( dd, ValueOffSet ); - /////////////////////////////////////////////////////////////// - fprintf( Output, " " ); - - if ( h != nCellsHor-1 ) - if ( h&1 ) - fprintf( Output, "%c", DOUBLE_VERTICAL ); - else - fprintf( Output, "%c", SINGLE_VERTICAL ); - } - fprintf( Output, "%c", DOUBLE_VERTICAL ); - fprintf( Output, "\n" ); - - Cudd_RecursiveDeref( dd, CubeVerBDD ); - - if ( v != nCellsVer-1 ) - // print separator line - { - for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); - if ( v&1 ) - { - fprintf( Output, "%c", D_JOINS_D_VER_RIGHT ); - for ( s = 0; s < nCellsHor; s++ ) - { - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - if ( s != nCellsHor-1 ) - if ( s&1 ) - fprintf( Output, "%c", DOUBLES_CROSS ); - else - fprintf( Output, "%c", S_VER_CROSS_D_HOR ); - } - fprintf( Output, "%c", D_JOINS_D_VER_LEFT ); - } - else - { - fprintf( Output, "%c", S_JOINS_D_VER_RIGHT ); - for ( s = 0; s < nCellsHor; s++ ) - { - fprintf( Output, "%c", SINGLE_HORIZONTAL ); - fprintf( Output, "%c", SINGLE_HORIZONTAL ); - fprintf( Output, "%c", SINGLE_HORIZONTAL ); - if ( s != nCellsHor-1 ) - if ( s&1 ) - fprintf( Output, "%c", S_HOR_CROSS_D_VER ); - else - fprintf( Output, "%c", SINGLES_CROSS ); - } - fprintf( Output, "%c", S_JOINS_D_VER_LEFT ); - } - fprintf( Output, "\n" ); - } - } - - //////////////////////////////////////////////////////////////////// - // print the lower line - for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); - fprintf( Output, "%c", DOUBLE_BOT_LEFT ); - for ( s = 0; s < nCellsHor; s++ ) - { - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - fprintf( Output, "%c", DOUBLE_HORIZONTAL ); - if ( s != nCellsHor-1 ) - if ( s&1 ) - fprintf( Output, "%c", D_JOINS_D_HOR_TOP ); - else - fprintf( Output, "%c", S_JOINS_D_HOR_TOP ); - } - fprintf( Output, "%c", DOUBLE_BOT_RIGHT ); - fprintf( Output, "\n" ); - - if ( !fHorizontalVarNamesPrintedAbove ) - { - //////////////////////////////////////////////////////////////////// - // print horizontal digits - for ( d = 0; d < nVarsHor; d++ ) - { - for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) ); - for ( n = 0; n < nCellsHor; n++ ) - if ( GrayCode(n) & (1<<(nVarsHor-1-d)) ) - fprintf( Output, "1 " ); - else - fprintf( Output, "0 " ); - - ///////////////////////////////// - fprintf( Output, "%c", (char)('a'+d) ); - ///////////////////////////////// - fprintf( Output, "\n" ); - } - } -} - - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int GrayCode ( int BinCode ) -{ - return BinCode ^ ( BinCode >> 1 ); -} - -/**Function******************************************************************** - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int BinCode ( int GrayCode ) -{ - int bc = GrayCode; - while( GrayCode >>= 1 ) bc ^= GrayCode; - return bc; -} - - diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c index a3320ad3..373ce5c5 100644 --- a/src/misc/extra/extraBddMisc.c +++ b/src/misc/extra/extraBddMisc.c @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: extraBddMisc.c,v 1.4 2005/10/04 00:19:54 alanmi Exp $] + Revision [$Id: extraBddMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -50,13 +50,10 @@ // file "extraDdTransfer.c" static DdNode * extraTransferPermuteRecur( DdManager * ddS, DdManager * ddD, DdNode * f, st_table * table, int * Permute ); static DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute ); -static DdNode * cuddBddPermuteRecur ARGS( ( DdManager * manager, DdHashTable * table, DdNode * node, int *permut ) ); // file "cuddUtils.c" -static void ddSupportStep(DdNode *f, int *support); -static void ddClearFlag(DdNode *f); - -static DdNode* extraZddPrimes( DdManager *dd, DdNode* F ); +static void ddSupportStep ARGS((DdNode *f, int *support)); +static void ddClearFlag ARGS((DdNode *f)); /**AutomaticEnd***************************************************************/ @@ -687,280 +684,6 @@ DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ) return bProd; } -/**Function******************************************************************** - - Synopsis [Computes the cube of BDD variables corresponding to bits it the bit-code] - - Description [Returns a bdd composed of elementary bdds found in array BddVars[] such - that the bdd vars encode the number Value of bit length CodeWidth (if fMsbFirst is 1, - the most significant bit is encoded with the first bdd variable). If the variables - BddVars are not specified, takes the first CodeWidth variables of the manager] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst ) -{ - int z; - DdNode * bTemp, * bVar, * bVarBdd, * bResult; - - bResult = b1; Cudd_Ref( bResult ); - for ( z = 0; z < CodeWidth; z++ ) - { - bVarBdd = (pbVars)? pbVars[z]: dd->vars[z]; - if ( fMsbFirst ) - bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (CodeWidth-1-z)))==0 ); - else - bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (z)))==0 ); - bResult = Cudd_bddAnd( dd, bTemp = bResult, bVar ); Cudd_Ref( bResult ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref( bResult ); - - return bResult; -} /* end of Extra_bddBitsToCube */ - -/**Function******************************************************************** - - Synopsis [Finds the support as a negative polarity cube.] - - Description [Finds the variables on which a DD depends. Returns a BDD - consisting of the product of the variables in the negative polarity - if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_VectorSupport Cudd_Support] - -******************************************************************************/ -DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f ) -{ - int *support; - DdNode *res, *tmp, *var; - int i, j; - int size; - - /* Allocate and initialize support array for ddSupportStep. */ - size = ddMax( dd->size, dd->sizeZ ); - support = ALLOC( int, size ); - if ( support == NULL ) - { - dd->errorCode = CUDD_MEMORY_OUT; - return ( NULL ); - } - for ( i = 0; i < size; i++ ) - { - support[i] = 0; - } - - /* Compute support and clean up markers. */ - ddSupportStep( Cudd_Regular( f ), support ); - ddClearFlag( Cudd_Regular( f ) ); - - /* Transform support from array to cube. */ - do - { - dd->reordered = 0; - res = DD_ONE( dd ); - cuddRef( res ); - for ( j = size - 1; j >= 0; j-- ) - { /* for each level bottom-up */ - i = ( j >= dd->size ) ? j : dd->invperm[j]; - if ( support[i] == 1 ) - { - var = cuddUniqueInter( dd, i, dd->one, Cudd_Not( dd->one ) ); - ////////////////////////////////////////////////////////////////// - var = Cudd_Not(var); - ////////////////////////////////////////////////////////////////// - cuddRef( var ); - tmp = cuddBddAndRecur( dd, res, var ); - if ( tmp == NULL ) - { - Cudd_RecursiveDeref( dd, res ); - Cudd_RecursiveDeref( dd, var ); - res = NULL; - break; - } - cuddRef( tmp ); - Cudd_RecursiveDeref( dd, res ); - Cudd_RecursiveDeref( dd, var ); - res = tmp; - } - } - } - while ( dd->reordered == 1 ); - - FREE( support ); - if ( res != NULL ) - cuddDeref( res ); - return ( res ); - -} /* end of Extra_SupportNeg */ - -/**Function******************************************************************** - - Synopsis [Returns 1 if the BDD is the BDD of elementary variable.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Extra_bddIsVar( DdNode * bFunc ) -{ - bFunc = Cudd_Regular( bFunc ); - if ( cuddIsConstant(bFunc) ) - return 0; - return cuddIsConstant( cuddT(bFunc) ) && cuddIsConstant( Cudd_Regular(cuddE(bFunc)) ); -} - -/**Function******************************************************************** - - Synopsis [Creates AND composed of the first nVars of the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddCreateAnd( DdManager * dd, int nVars ) -{ - DdNode * bFunc, * bTemp; - int i; - bFunc = Cudd_ReadOne(dd); Cudd_Ref( bFunc ); - for ( i = 0; i < nVars; i++ ) - { - bFunc = Cudd_bddAnd( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) ); Cudd_Ref( bFunc ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref( bFunc ); - return bFunc; -} - -/**Function******************************************************************** - - Synopsis [Creates OR composed of the first nVars of the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddCreateOr( DdManager * dd, int nVars ) -{ - DdNode * bFunc, * bTemp; - int i; - bFunc = Cudd_ReadLogicZero(dd); Cudd_Ref( bFunc ); - for ( i = 0; i < nVars; i++ ) - { - bFunc = Cudd_bddOr( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) ); Cudd_Ref( bFunc ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref( bFunc ); - return bFunc; -} - -/**Function******************************************************************** - - Synopsis [Creates EXOR composed of the first nVars of the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddCreateExor( DdManager * dd, int nVars ) -{ - DdNode * bFunc, * bTemp; - int i; - bFunc = Cudd_ReadLogicZero(dd); Cudd_Ref( bFunc ); - for ( i = 0; i < nVars; i++ ) - { - bFunc = Cudd_bddXor( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) ); Cudd_Ref( bFunc ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref( bFunc ); - return bFunc; -} - -/**Function******************************************************************** - - Synopsis [Computes the set of primes as a ZDD.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F ) -{ - DdNode *res; - do { - dd->reordered = 0; - res = extraZddPrimes(dd, F); - if ( dd->reordered == 1 ) - printf("\nReordering in Extra_zddPrimes()\n"); - } while (dd->reordered == 1); - return(res); - -} /* end of Extra_zddPrimes */ - -/**Function******************************************************************** - - Synopsis [Permutes the variables of the array of BDDs.] - - Description [Given a permutation in array permut, creates a new BDD - with permuted variables. There should be an entry in array permut - for each variable in the manager. The i-th entry of permut holds the - index of the variable that is to substitute the i-th variable. - The DDs in the resulting array are already referenced.] - - SideEffects [None] - - SeeAlso [Cudd_addPermute Cudd_bddSwapVariables] - -******************************************************************************/ -void Extra_bddPermuteArray( DdManager * manager, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut ) -{ - DdHashTable *table; - int i, k; - do - { - manager->reordered = 0; - table = cuddHashTableInit( manager, 1, 2 ); - - /* permute the output functions one-by-one */ - for ( i = 0; i < nNodes; i++ ) - { - bNodesOut[i] = cuddBddPermuteRecur( manager, table, bNodesIn[i], permut ); - if ( bNodesOut[i] == NULL ) - { - /* deref the array of the already computed outputs */ - for ( k = 0; k < i; k++ ) - Cudd_RecursiveDeref( manager, bNodesOut[k] ); - break; - } - cuddRef( bNodesOut[i] ); - } - /* Dispose of local cache. */ - cuddHashTableQuit( table ); - } - while ( manager->reordered == 1 ); -} /* end of Extra_bddPermuteArray */ - - /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ @@ -1316,297 +1039,6 @@ ddClearFlag( } /* end of ddClearFlag */ -/**Function******************************************************************** - - Synopsis [Composed three subcovers into one ZDD.] - - Description [] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -DdNode * -extraComposeCover( - DdManager* dd, /* the manager */ - DdNode* zC0, /* the pointer to the negative var cofactor */ - DdNode* zC1, /* the pointer to the positive var cofactor */ - DdNode* zC2, /* the pointer to the cofactor without var */ - int TopVar) /* the index of the positive ZDD var */ -{ - DdNode * zRes, * zTemp; - /* compose with-neg-var and without-var using the neg ZDD var */ - zTemp = cuddZddGetNode( dd, 2*TopVar + 1, zC0, zC2 ); - if ( zTemp == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zC0); - Cudd_RecursiveDerefZdd(dd, zC1); - Cudd_RecursiveDerefZdd(dd, zC2); - return NULL; - } - cuddRef( zTemp ); - cuddDeref( zC0 ); - cuddDeref( zC2 ); - - /* compose with-pos-var and previous result using the pos ZDD var */ - zRes = cuddZddGetNode( dd, 2*TopVar, zC1, zTemp ); - if ( zRes == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zC1); - Cudd_RecursiveDerefZdd(dd, zTemp); - return NULL; - } - cuddDeref( zC1 ); - cuddDeref( zTemp ); - return zRes; -} /* extraComposeCover */ - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of prime computation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode* extraZddPrimes( DdManager *dd, DdNode* F ) -{ - DdNode *zRes; - - if ( F == Cudd_Not( dd->one ) ) - return dd->zero; - if ( F == dd->one ) - return dd->one; - - /* check cache */ - zRes = cuddCacheLookup1Zdd(dd, extraZddPrimes, F); - if (zRes) - return(zRes); - { - /* temporary variables */ - DdNode *bF01, *zP0, *zP1; - /* three components of the prime set */ - DdNode *zResE, *zResP, *zResN; - int fIsComp = Cudd_IsComplement( F ); - - /* find cofactors of F */ - DdNode * bF0 = Cudd_NotCond( Cudd_E( F ), fIsComp ); - DdNode * bF1 = Cudd_NotCond( Cudd_T( F ), fIsComp ); - - /* find the intersection of cofactors */ - bF01 = cuddBddAndRecur( dd, bF0, bF1 ); - if ( bF01 == NULL ) return NULL; - cuddRef( bF01 ); - - /* solve the problems for cofactors */ - zP0 = extraZddPrimes( dd, bF0 ); - if ( zP0 == NULL ) - { - Cudd_RecursiveDeref( dd, bF01 ); - return NULL; - } - cuddRef( zP0 ); - - zP1 = extraZddPrimes( dd, bF1 ); - if ( zP1 == NULL ) - { - Cudd_RecursiveDeref( dd, bF01 ); - Cudd_RecursiveDerefZdd( dd, zP0 ); - return NULL; - } - cuddRef( zP1 ); - - /* check for local unateness */ - if ( bF01 == bF0 ) /* unate increasing */ - { - /* intersection is useless */ - cuddDeref( bF01 ); - /* the primes of intersection are the primes of F0 */ - zResE = zP0; - /* there are no primes with negative var */ - zResN = dd->zero; - cuddRef( zResN ); - /* primes with positive var are primes of F1 that are not primes of F01 */ - zResP = cuddZddDiff( dd, zP1, zP0 ); - if ( zResP == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zResE ); - Cudd_RecursiveDerefZdd( dd, zResN ); - Cudd_RecursiveDerefZdd( dd, zP1 ); - return NULL; - } - cuddRef( zResP ); - Cudd_RecursiveDerefZdd( dd, zP1 ); - } - else if ( bF01 == bF1 ) /* unate decreasing */ - { - /* intersection is useless */ - cuddDeref( bF01 ); - /* the primes of intersection are the primes of F1 */ - zResE = zP1; - /* there are no primes with positive var */ - zResP = dd->zero; - cuddRef( zResP ); - /* primes with negative var are primes of F0 that are not primes of F01 */ - zResN = cuddZddDiff( dd, zP0, zP1 ); - if ( zResN == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zResE ); - Cudd_RecursiveDerefZdd( dd, zResP ); - Cudd_RecursiveDerefZdd( dd, zP0 ); - return NULL; - } - cuddRef( zResN ); - Cudd_RecursiveDerefZdd( dd, zP0 ); - } - else /* not unate */ - { - /* primes without the top var are primes of F10 */ - zResE = extraZddPrimes( dd, bF01 ); - if ( zResE == NULL ) - { - Cudd_RecursiveDerefZdd( dd, bF01 ); - Cudd_RecursiveDerefZdd( dd, zP0 ); - Cudd_RecursiveDerefZdd( dd, zP1 ); - return NULL; - } - cuddRef( zResE ); - Cudd_RecursiveDeref( dd, bF01 ); - - /* primes with the negative top var are those of P0 that are not in F10 */ - zResN = cuddZddDiff( dd, zP0, zResE ); - if ( zResN == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zResE ); - Cudd_RecursiveDerefZdd( dd, zP0 ); - Cudd_RecursiveDerefZdd( dd, zP1 ); - return NULL; - } - cuddRef( zResN ); - Cudd_RecursiveDerefZdd( dd, zP0 ); - - /* primes with the positive top var are those of P1 that are not in F10 */ - zResP = cuddZddDiff( dd, zP1, zResE ); - if ( zResP == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zResE ); - Cudd_RecursiveDerefZdd( dd, zResN ); - Cudd_RecursiveDerefZdd( dd, zP1 ); - return NULL; - } - cuddRef( zResP ); - Cudd_RecursiveDerefZdd( dd, zP1 ); - } - - zRes = extraComposeCover( dd, zResN, zResP, zResE, Cudd_Regular(F)->index ); - if ( zRes == NULL ) return NULL; - - /* insert the result into cache */ - cuddCacheInsert1(dd, extraZddPrimes, F, zRes); - return zRes; - } -} /* end of extraZddPrimes */ - -/**Function******************************************************************** - - Synopsis [Implements the recursive step of Cudd_bddPermute.] - - Description [ Recursively puts the BDD in the order given in the array permut. - Checks for trivial cases to terminate recursion, then splits on the - children of this node. Once the solutions for the children are - obtained, it puts into the current position the node from the rest of - the BDD that should be here. Then returns this BDD. - The key here is that the node being visited is NOT put in its proper - place by this instance, but rather is switched when its proper position - is reached in the recursion tree.<p> - The DdNode * that is returned is the same BDD as passed in as node, - but in the new order.] - - SideEffects [None] - - SeeAlso [Cudd_bddPermute cuddAddPermuteRecur] - -******************************************************************************/ -static DdNode * -cuddBddPermuteRecur( DdManager * manager /* DD manager */ , - DdHashTable * table /* computed table */ , - DdNode * node /* BDD to be reordered */ , - int *permut /* permutation array */ ) -{ - DdNode *N, *T, *E; - DdNode *res; - int index; - - statLine( manager ); - N = Cudd_Regular( node ); - - /* Check for terminal case of constant node. */ - if ( cuddIsConstant( N ) ) - { - return ( node ); - } - - /* If problem already solved, look up answer and return. */ - if ( N->ref != 1 && ( res = cuddHashTableLookup1( table, N ) ) != NULL ) - { -#ifdef DD_DEBUG - bddPermuteRecurHits++; -#endif - return ( Cudd_NotCond( res, N != node ) ); - } - - /* Split and recur on children of this node. */ - T = cuddBddPermuteRecur( manager, table, cuddT( N ), permut ); - if ( T == NULL ) - return ( NULL ); - cuddRef( T ); - E = cuddBddPermuteRecur( manager, table, cuddE( N ), permut ); - if ( E == NULL ) - { - Cudd_IterDerefBdd( manager, T ); - return ( NULL ); - } - cuddRef( E ); - - /* Move variable that should be in this position to this position - ** by retrieving the single var BDD for that variable, and calling - ** cuddBddIteRecur with the T and E we just created. - */ - index = permut[N->index]; - res = cuddBddIteRecur( manager, manager->vars[index], T, E ); - if ( res == NULL ) - { - Cudd_IterDerefBdd( manager, T ); - Cudd_IterDerefBdd( manager, E ); - return ( NULL ); - } - cuddRef( res ); - Cudd_IterDerefBdd( manager, T ); - Cudd_IterDerefBdd( manager, E ); - - /* Do not keep the result if the reference count is only 1, since - ** it will not be visited again. - */ - if ( N->ref != 1 ) - { - ptrint fanout = ( ptrint ) N->ref; - cuddSatDec( fanout ); - if ( !cuddHashTableInsert1( table, N, res, fanout ) ) - { - Cudd_IterDerefBdd( manager, res ); - return ( NULL ); - } - } - cuddDeref( res ); - return ( Cudd_NotCond( res, N != node ) ); - -} /* end of cuddBddPermuteRecur */ - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/extra/extraBddSymm.c b/src/misc/extra/extraBddSymm.c index 358402b0..474f663f 100644 --- a/src/misc/extra/extraBddSymm.c +++ b/src/misc/extra/extraBddSymm.c @@ -223,7 +223,7 @@ Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars ) /**Function******************************************************************** - Synopsis [Deallocates symmetry information structure.] + Synopsis [Delocates symmetry information structure.] Description [] diff --git a/src/misc/extra/extraBddUnate.c b/src/misc/extra/extraBddUnate.c deleted file mode 100644 index b0297c77..00000000 --- a/src/misc/extra/extraBddUnate.c +++ /dev/null @@ -1,641 +0,0 @@ -/**CFile**************************************************************** - - FileName [extraBddUnate.c] - - PackageName [extra] - - Synopsis [Efficient methods to compute the information about - unate variables using an algorithm that is conceptually similar to - the algorithm for two-variable symmetry computation presented in: - A. Mishchenko. Fast Computation of Symmetries in Boolean Functions. - Transactions on CAD, Nov. 2003.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 2.0. Started - September 1, 2003.] - - Revision [$Id: extraBddUnate.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "extra.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -/**AutomaticEnd***************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Computes the classical symmetry information for the function.] - - Description [Returns the symmetry information in the form of Extra_UnateInfo_t structure.] - - SideEffects [If the ZDD variables are not derived from BDD variables with - multiplicity 2, this function may derive them in a wrong way.] - - SeeAlso [] - -******************************************************************************/ -Extra_UnateInfo_t * Extra_UnateComputeFast( - DdManager * dd, /* the manager */ - DdNode * bFunc) /* the function whose symmetries are computed */ -{ - DdNode * bSupp; - DdNode * zRes; - Extra_UnateInfo_t * p; - - bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp ); - zRes = Extra_zddUnateInfoCompute( dd, bFunc, bSupp ); Cudd_Ref( zRes ); - - p = Extra_UnateInfoCreateFromZdd( dd, zRes, bSupp ); - - Cudd_RecursiveDeref( dd, bSupp ); - Cudd_RecursiveDerefZdd( dd, zRes ); - - return p; - -} /* end of Extra_UnateInfoCompute */ - - -/**Function******************************************************************** - - Synopsis [Computes the classical symmetry information as a ZDD.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_zddUnateInfoCompute( - DdManager * dd, /* the DD manager */ - DdNode * bF, - DdNode * bVars) -{ - DdNode * res; - do { - dd->reordered = 0; - res = extraZddUnateInfoCompute( dd, bF, bVars ); - } while (dd->reordered == 1); - return(res); - -} /* end of Extra_zddUnateInfoCompute */ - - -/**Function******************************************************************** - - Synopsis [Converts a set of variables into a set of singleton subsets.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_zddGetSingletonsBoth( - DdManager * dd, /* the DD manager */ - DdNode * bVars) /* the set of variables */ -{ - DdNode * res; - do { - dd->reordered = 0; - res = extraZddGetSingletonsBoth( dd, bVars ); - } while (dd->reordered == 1); - return(res); - -} /* end of Extra_zddGetSingletonsBoth */ - -/**Function******************************************************************** - - Synopsis [Allocates unateness information structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -Extra_UnateInfo_t * Extra_UnateInfoAllocate( int nVars ) -{ - Extra_UnateInfo_t * p; - // allocate and clean the storage for unateness info - p = ALLOC( Extra_UnateInfo_t, 1 ); - memset( p, 0, sizeof(Extra_UnateInfo_t) ); - p->nVars = nVars; - p->pVars = ALLOC( Extra_UnateVar_t, nVars ); - memset( p->pVars, 0, nVars * sizeof(Extra_UnateVar_t) ); - return p; -} /* end of Extra_UnateInfoAllocate */ - -/**Function******************************************************************** - - Synopsis [Deallocates symmetry information structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -void Extra_UnateInfoDissolve( Extra_UnateInfo_t * p ) -{ - free( p->pVars ); - free( p ); -} /* end of Extra_UnateInfoDissolve */ - -/**Function******************************************************************** - - Synopsis [Allocates symmetry information structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -void Extra_UnateInfoPrint( Extra_UnateInfo_t * p ) -{ - char * pBuffer; - int i; - pBuffer = ALLOC( char, p->nVarsMax+1 ); - memset( pBuffer, ' ', p->nVarsMax ); - pBuffer[p->nVarsMax] = 0; - for ( i = 0; i < p->nVars; i++ ) - if ( p->pVars[i].Neg ) - pBuffer[ p->pVars[i].iVar ] = 'n'; - else if ( p->pVars[i].Pos ) - pBuffer[ p->pVars[i].iVar ] = 'p'; - else - pBuffer[ p->pVars[i].iVar ] = '.'; - printf( "%s\n", pBuffer ); - free( pBuffer ); -} /* end of Extra_UnateInfoPrint */ - - -/**Function******************************************************************** - - Synopsis [Creates the symmetry information structure from ZDD.] - - Description [ZDD representation of symmetries is the set of cubes, each - of which has two variables in the positive polarity. These variables correspond - to the symmetric variable pair.] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bSupp ) -{ - Extra_UnateInfo_t * p; - DdNode * bTemp, * zSet, * zCube, * zTemp; - int * pMapVars2Nums; - int i, nSuppSize; - - nSuppSize = Extra_bddSuppSize( dd, bSupp ); - - // allocate and clean the storage for symmetry info - p = Extra_UnateInfoAllocate( nSuppSize ); - - // allocate the storage for the temporary map - pMapVars2Nums = ALLOC( int, dd->size ); - memset( pMapVars2Nums, 0, dd->size * sizeof(int) ); - - // assign the variables - p->nVarsMax = dd->size; - for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ ) - { - p->pVars[i].iVar = bTemp->index; - pMapVars2Nums[bTemp->index] = i; - } - - // write the symmetry info into the structure - zSet = zPairs; Cudd_Ref( zSet ); -// Cudd_zddPrintCover( dd, zPairs ); printf( "\n" ); - while ( zSet != z0 ) - { - // get the next cube - zCube = Extra_zddSelectOneSubset( dd, zSet ); Cudd_Ref( zCube ); - - // add this var to the data structure - assert( cuddT(zCube) == z1 && cuddE(zCube) == z0 ); - if ( zCube->index & 1 ) // neg - p->pVars[ pMapVars2Nums[zCube->index/2] ].Neg = 1; - else - p->pVars[ pMapVars2Nums[zCube->index/2] ].Pos = 1; - // count the unate vars - p->nUnate++; - - // update the cuver and deref the cube - zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube ); Cudd_Ref( zSet ); - Cudd_RecursiveDerefZdd( dd, zTemp ); - Cudd_RecursiveDerefZdd( dd, zCube ); - - } // for each cube - Cudd_RecursiveDerefZdd( dd, zSet ); - FREE( pMapVars2Nums ); - return p; - -} /* end of Extra_UnateInfoCreateFromZdd */ - - - -/**Function******************************************************************** - - Synopsis [Computes the classical unateness information for the function.] - - Description [Uses the naive way of comparing cofactors.] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -Extra_UnateInfo_t * Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc ) -{ - int nSuppSize; - DdNode * bSupp, * bTemp; - Extra_UnateInfo_t * p; - int i, Res; - - // compute the support - bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp ); - nSuppSize = Extra_bddSuppSize( dd, bSupp ); -//printf( "Support = %d. ", nSuppSize ); -//Extra_bddPrint( dd, bSupp ); -//printf( "%d ", nSuppSize ); - - // allocate the storage for symmetry info - p = Extra_UnateInfoAllocate( nSuppSize ); - - // assign the variables - p->nVarsMax = dd->size; - for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ ) - { - Res = Extra_bddCheckUnateNaive( dd, bFunc, bTemp->index ); - p->pVars[i].iVar = bTemp->index; - if ( Res == -1 ) - p->pVars[i].Neg = 1; - else if ( Res == 1 ) - p->pVars[i].Pos = 1; - p->nUnate += (Res != 0); - } - Cudd_RecursiveDeref( dd, bSupp ); - return p; - -} /* end of Extra_UnateComputeSlow */ - -/**Function******************************************************************** - - Synopsis [Checks if the two variables are symmetric.] - - Description [Returns 0 if vars are not unate. Return -1/+1 if the var is neg/pos unate.] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Extra_bddCheckUnateNaive( - DdManager * dd, /* the DD manager */ - DdNode * bF, - int iVar) -{ - DdNode * bCof0, * bCof1; - int Res; - - assert( iVar < dd->size ); - - bCof0 = Cudd_Cofactor( dd, bF, Cudd_Not(Cudd_bddIthVar(dd,iVar)) ); Cudd_Ref( bCof0 ); - bCof1 = Cudd_Cofactor( dd, bF, Cudd_bddIthVar(dd,iVar) ); Cudd_Ref( bCof1 ); - - if ( Cudd_bddLeq( dd, bCof0, bCof1 ) ) - Res = 1; - else if ( Cudd_bddLeq( dd, bCof1, bCof0 ) ) - Res =-1; - else - Res = 0; - - Cudd_RecursiveDeref( dd, bCof0 ); - Cudd_RecursiveDeref( dd, bCof1 ); - return Res; -} /* end of Extra_bddCheckUnateNaive */ - - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Performs a recursive step of Extra_UnateInfoCompute.] - - Description [Returns the set of symmetric variable pairs represented as a set - of two-literal ZDD cubes. Both variables always appear in the positive polarity - in the cubes. This function works without building new BDD nodes. Some relatively - small number of ZDD nodes may be built to ensure proper bookkeeping of the - symmetry information.] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * -extraZddUnateInfoCompute( - DdManager * dd, /* the manager */ - DdNode * bFunc, /* the function whose symmetries are computed */ - DdNode * bVars ) /* the set of variables on which this function depends */ -{ - DdNode * zRes; - DdNode * bFR = Cudd_Regular(bFunc); - - if ( cuddIsConstant(bFR) ) - { - if ( cuddIsConstant(bVars) ) - return z0; - return extraZddGetSingletonsBoth( dd, bVars ); - } - assert( bVars != b1 ); - - if ( zRes = cuddCacheLookup2Zdd(dd, extraZddUnateInfoCompute, bFunc, bVars) ) - return zRes; - else - { - DdNode * zRes0, * zRes1; - DdNode * zTemp, * zPlus; - DdNode * bF0, * bF1; - DdNode * bVarsNew; - int nVarsExtra; - int LevelF; - int AddVar; - - // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV - // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F - // count how many extra vars are there in bVars - nVarsExtra = 0; - LevelF = dd->perm[bFR->index]; - for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) ) - nVarsExtra++; - // the indexes (level) of variables should be synchronized now - assert( bFR->index == bVarsNew->index ); - - // cofactor the function - if ( bFR != bFunc ) // bFunc is complemented - { - bF0 = Cudd_Not( cuddE(bFR) ); - bF1 = Cudd_Not( cuddT(bFR) ); - } - else - { - bF0 = cuddE(bFR); - bF1 = cuddT(bFR); - } - - // solve subproblems - zRes0 = extraZddUnateInfoCompute( dd, bF0, cuddT(bVarsNew) ); - if ( zRes0 == NULL ) - return NULL; - cuddRef( zRes0 ); - - // if there is no symmetries in the negative cofactor - // there is no need to test the positive cofactor - if ( zRes0 == z0 ) - zRes = zRes0; // zRes takes reference - else - { - zRes1 = extraZddUnateInfoCompute( dd, bF1, cuddT(bVarsNew) ); - if ( zRes1 == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zRes0 ); - return NULL; - } - cuddRef( zRes1 ); - - // only those variables are pair-wise symmetric - // that are pair-wise symmetric in both cofactors - // therefore, intersect the solutions - zRes = cuddZddIntersect( dd, zRes0, zRes1 ); - if ( zRes == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zRes0 ); - Cudd_RecursiveDerefZdd( dd, zRes1 ); - return NULL; - } - cuddRef( zRes ); - Cudd_RecursiveDerefZdd( dd, zRes0 ); - Cudd_RecursiveDerefZdd( dd, zRes1 ); - } - - // consider the current top-most variable - AddVar = -1; - if ( Cudd_bddLeq( dd, bF0, bF1 ) ) // pos - AddVar = 0; - else if ( Cudd_bddLeq( dd, bF1, bF0 ) ) // neg - AddVar = 1; - if ( AddVar >= 0 ) - { - // create the singleton - zPlus = cuddZddGetNode( dd, 2*bFR->index + AddVar, z1, z0 ); - if ( zPlus == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zRes ); - return NULL; - } - cuddRef( zPlus ); - - // add these to the result - zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); - if ( zRes == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zTemp ); - Cudd_RecursiveDerefZdd( dd, zPlus ); - return NULL; - } - cuddRef( zRes ); - Cudd_RecursiveDerefZdd( dd, zTemp ); - Cudd_RecursiveDerefZdd( dd, zPlus ); - } - // only zRes is referenced at this point - - // if we skipped some variables, these variables cannot be symmetric with - // any variables that are currently in the support of bF, but they can be - // symmetric with the variables that are in bVars but not in the support of bF - for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) ) - { - // create the negative singleton - zPlus = cuddZddGetNode( dd, 2*bVarsNew->index+1, z1, z0 ); - if ( zPlus == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zRes ); - return NULL; - } - cuddRef( zPlus ); - - // add these to the result - zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); - if ( zRes == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zTemp ); - Cudd_RecursiveDerefZdd( dd, zPlus ); - return NULL; - } - cuddRef( zRes ); - Cudd_RecursiveDerefZdd( dd, zTemp ); - Cudd_RecursiveDerefZdd( dd, zPlus ); - - - // create the positive singleton - zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 ); - if ( zPlus == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zRes ); - return NULL; - } - cuddRef( zPlus ); - - // add these to the result - zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); - if ( zRes == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zTemp ); - Cudd_RecursiveDerefZdd( dd, zPlus ); - return NULL; - } - cuddRef( zRes ); - Cudd_RecursiveDerefZdd( dd, zTemp ); - Cudd_RecursiveDerefZdd( dd, zPlus ); - } - cuddDeref( zRes ); - - /* insert the result into cache */ - cuddCacheInsert2(dd, extraZddUnateInfoCompute, bFunc, bVars, zRes); - return zRes; - } -} /* end of extraZddUnateInfoCompute */ - - -/**Function******************************************************************** - - Synopsis [Performs a recursive step of Extra_zddGetSingletons.] - - Description [Returns the set of ZDD singletons, containing those pos/neg - polarity ZDD variables that correspond to the BDD variables in bVars.] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * extraZddGetSingletonsBoth( - DdManager * dd, /* the DD manager */ - DdNode * bVars) /* the set of variables */ -{ - DdNode * zRes; - - if ( bVars == b1 ) - return z1; - - if ( zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletonsBoth, bVars) ) - return zRes; - else - { - DdNode * zTemp, * zPlus; - - // solve subproblem - zRes = extraZddGetSingletonsBoth( dd, cuddT(bVars) ); - if ( zRes == NULL ) - return NULL; - cuddRef( zRes ); - - - // create the negative singleton - zPlus = cuddZddGetNode( dd, 2*bVars->index+1, z1, z0 ); - if ( zPlus == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zRes ); - return NULL; - } - cuddRef( zPlus ); - - // add these to the result - zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); - if ( zRes == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zTemp ); - Cudd_RecursiveDerefZdd( dd, zPlus ); - return NULL; - } - cuddRef( zRes ); - Cudd_RecursiveDerefZdd( dd, zTemp ); - Cudd_RecursiveDerefZdd( dd, zPlus ); - - - // create the positive singleton - zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 ); - if ( zPlus == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zRes ); - return NULL; - } - cuddRef( zPlus ); - - // add these to the result - zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); - if ( zRes == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zTemp ); - Cudd_RecursiveDerefZdd( dd, zPlus ); - return NULL; - } - cuddRef( zRes ); - Cudd_RecursiveDerefZdd( dd, zTemp ); - Cudd_RecursiveDerefZdd( dd, zPlus ); - - cuddDeref( zRes ); - cuddCacheInsert1( dd, extraZddGetSingletonsBoth, bVars, zRes ); - return zRes; - } -} /* end of extraZddGetSingletonsBoth */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static Functions */ -/*---------------------------------------------------------------------------*/ diff --git a/src/misc/extra/extraUtilBitMatrix.c b/src/misc/extra/extraUtilBitMatrix.c index b860a538..93cbbeac 100644 --- a/src/misc/extra/extraUtilBitMatrix.c +++ b/src/misc/extra/extraUtilBitMatrix.c @@ -348,7 +348,7 @@ int Extra_BitMatrixCountOnesUpper( Extra_BitMat_t * p ) int i, k, nTotal = 0; for ( i = 0; i < p->nSize; i++ ) for ( k = i + 1; k < p->nSize; k++ ) - nTotal += ( (p->ppData[i][k>>5] & (1 << (k&31))) > 0 ); + nTotal += ( (p->ppData[i][k/32] & (1 << (k%32))) > 0 ); return nTotal; } diff --git a/src/misc/extra/extraUtilCanon.c b/src/misc/extra/extraUtilCanon.c index fcc7d84d..9d4e5b5d 100644 --- a/src/misc/extra/extraUtilCanon.c +++ b/src/misc/extra/extraUtilCanon.c @@ -99,8 +99,7 @@ int Extra_TruthCanonFastN( int nVarsMax, int nVarsReal, unsigned * pt, unsigned Description [] - SideEffects [This procedure has a bug, which shows on Solaris. - Most likely has something to do with the casts, i.g *((unsigned *)pt0)] + SideEffects [] SeeAlso [] @@ -130,22 +129,21 @@ int Extra_TruthCanonN_rec( int nVars, unsigned char * pt, unsigned ** pptRes, ch pt0 = pt; pt1 = pt + (1 << nVarsN) / 8; // 5-var truth tables for this call -// uInit0 = *((unsigned *)pt0); -// uInit1 = *((unsigned *)pt1); + uInit0 = *((unsigned *)pt0); + uInit1 = *((unsigned *)pt1); if ( nVarsN == 3 ) { - uInit0 = (pt0[0] << 24) | (pt0[0] << 16) | (pt0[0] << 8) | pt0[0]; - uInit1 = (pt1[0] << 24) | (pt1[0] << 16) | (pt1[0] << 8) | pt1[0]; + uInit0 &= 0xFF; + uInit1 &= 0xFF; + uInit0 = (uInit0 << 24) | (uInit0 << 16) | (uInit0 << 8) | uInit0; + uInit1 = (uInit1 << 24) | (uInit1 << 16) | (uInit1 << 8) | uInit1; } else if ( nVarsN == 4 ) { - uInit0 = (pt0[1] << 24) | (pt0[0] << 16) | (pt0[1] << 8) | pt0[0]; - uInit1 = (pt1[1] << 24) | (pt1[0] << 16) | (pt1[1] << 8) | pt1[0]; - } - else - { - uInit0 = (pt0[3] << 24) | (pt0[2] << 16) | (pt0[1] << 8) | pt0[0]; - uInit1 = (pt1[3] << 24) | (pt1[2] << 16) | (pt1[1] << 8) | pt1[0]; + uInit0 &= 0xFFFF; + uInit1 &= 0xFFFF; + uInit0 = (uInit0 << 16) | uInit0; + uInit1 = (uInit1 << 16) | uInit1; } // storage for truth tables and phases diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c index 4c51b8b5..03b31fea 100644 --- a/src/misc/extra/extraUtilFile.c +++ b/src/misc/extra/extraUtilFile.c @@ -110,7 +110,7 @@ char * Extra_FileGetSimilarName( char * pFileNameWrong, char * pS1, char * pS2, /**Function************************************************************* - Synopsis [Returns the pointer to the file extension.] + Synopsis [] Description [] @@ -119,14 +119,21 @@ char * Extra_FileGetSimilarName( char * pFileNameWrong, char * pS1, char * pS2, SeeAlso [] ***********************************************************************/ -char * Extra_FileNameExtension( char * FileName ) +int Extra_FileNameCheckExtension( char * FileName, char * Extension ) { char * pDot; - // find the last "dot" in the file name, if it is present + // find "dot" if it is present in the file name +// pDot = strstr( FileName, "." ); for ( pDot = FileName + strlen(FileName)-1; pDot >= FileName; pDot-- ) if ( *pDot == '.' ) - return pDot + 1; - return NULL; + break; + if ( *pDot != '.' ) + return 0; + // check the extension + if ( pDot && strcmp( pDot+1, Extension ) == 0 ) + return 1; + else + return 0; } /**Function************************************************************* @@ -165,7 +172,7 @@ char * Extra_FileNameGeneric( char * FileName ) char * pRes; // find the generic name of the file - pRes = Extra_UtilStrsav( FileName ); + pRes = util_strsav( FileName ); // find the pointer to the "." symbol in the file name // pUnd = strstr( FileName, "_" ); pUnd = NULL; @@ -248,8 +255,8 @@ char * Extra_FileRead( FILE * pFile ) char * Extra_TimeStamp() { static char Buffer[100]; - char * TimeStamp; time_t ltime; + char * TimeStamp; // get the current time time( <ime ); TimeStamp = asctime( localtime( <ime ) ); @@ -313,97 +320,6 @@ void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits ) /**Function************************************************************* - Synopsis [Reads the hex unsigned into the bit-string.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Extra_ReadHexadecimal( unsigned Sign[], char * pString, int nVars ) -{ - int nWords, nDigits, Digit, k, c; - nWords = Extra_TruthWordNum( nVars ); - for ( k = 0; k < nWords; k++ ) - Sign[k] = 0; - // read the number from the string - nDigits = (1 << nVars) / 4; - if ( nDigits == 0 ) - nDigits = 1; - for ( k = 0; k < nDigits; k++ ) - { - c = nDigits-1-k; - if ( pString[c] >= '0' && pString[c] <= '9' ) - Digit = pString[c] - '0'; - else if ( pString[c] >= 'A' && pString[c] <= 'F' ) - Digit = pString[c] - 'A' + 10; - else if ( pString[c] >= 'a' && pString[c] <= 'f' ) - Digit = pString[c] - 'a' + 10; - else { assert( 0 ); return 0; } - Sign[k/8] |= ( (Digit & 15) << ((k%8) * 4) ); - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Prints the hex unsigned into a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars ) -{ - int nDigits, Digit, k; - // write the number into the file - nDigits = (1 << nVars) / 4; - for ( k = nDigits - 1; k >= 0; k-- ) - { - Digit = ((Sign[k/8] >> ((k%8) * 4)) & 15); - if ( Digit < 10 ) - fprintf( pFile, "%d", Digit ); - else - fprintf( pFile, "%c", 'a' + Digit-10 ); - } -// fprintf( pFile, "\n" ); -} - -/**Function************************************************************* - - Synopsis [Prints the hex unsigned into a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_PrintHexadecimalString( char * pString, unsigned Sign[], int nVars ) -{ - int nDigits, Digit, k; - // write the number into the file - nDigits = (1 << nVars) / 4; - for ( k = nDigits - 1; k >= 0; k-- ) - { - Digit = ((Sign[k/8] >> ((k%8) * 4)) & 15); - if ( Digit < 10 ) - *pString++ = '0' + Digit; - else - *pString++ = 'a' + Digit-10; - } -// fprintf( pFile, "\n" ); - *pString = 0; -} - -/**Function************************************************************* - Synopsis [Prints the hex unsigned into a file.] Description [] @@ -475,7 +391,7 @@ char * Extra_StringAppend( char * pStrGiven, char * pStrAdd ) free( pStrGiven ); } else - pTemp = Extra_UtilStrsav( pStrAdd ); + pTemp = util_strsav( pStrAdd ); return pTemp; } diff --git a/src/misc/extra/extraUtilMemory.c b/src/misc/extra/extraUtilMemory.c index 6eccf015..af1128ac 100644 --- a/src/misc/extra/extraUtilMemory.c +++ b/src/misc/extra/extraUtilMemory.c @@ -73,9 +73,6 @@ struct Extra_MmStep_t_ Extra_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc int nMapSize; // the size of the memory array Extra_MmFixed_t ** pMap; // maps the number of bytes into its memory manager - int nLargeChunksAlloc; // the maximum number of large memory chunks - int nLargeChunks; // the current number of large memory chunks - void ** pLargeChunks; // the allocated large memory chunks }; /*---------------------------------------------------------------------------*/ @@ -155,30 +152,18 @@ Extra_MmFixed_t * Extra_MmFixedStart( int nEntrySize ) SeeAlso [] ***********************************************************************/ -void Extra_MmFixedPrint( Extra_MmFixed_t * p ) -{ - printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n", - p->nEntrySize, p->nChunkSize, p->nChunks ); - printf( " Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n", - p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_MmFixedStop( Extra_MmFixed_t * p ) +void Extra_MmFixedStop( Extra_MmFixed_t * p, int fVerbose ) { int i; if ( p == NULL ) return; + if ( fVerbose ) + { + printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n", + p->nEntrySize, p->nChunkSize, p->nChunks ); + printf( " Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n", + p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc ); + } for ( i = 0; i < p->nChunks; i++ ) free( p->pChunks[i] ); free( p->pChunks ); @@ -272,7 +257,7 @@ void Extra_MmFixedRestart( Extra_MmFixed_t * p ) int i; char * pTemp; - // deallocate all chunks except the first one + // delocate all chunks except the first one for ( i = 1; i < p->nChunks; i++ ) free( p->pChunks[i] ); p->nChunks = 1; @@ -310,21 +295,6 @@ int Extra_MmFixedReadMemUsage( Extra_MmFixed_t * p ) return p->nMemoryAlloc; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Extra_MmFixedReadMaxEntriesUsed( Extra_MmFixed_t * p ) -{ - return p->nEntriesMax; -} /**Function************************************************************* @@ -341,7 +311,7 @@ int Extra_MmFixedReadMaxEntriesUsed( Extra_MmFixed_t * p ) Extra_MmFlex_t * Extra_MmFlexStart() { Extra_MmFlex_t * p; -//printf( "allocing flex\n" ); + p = ALLOC( Extra_MmFlex_t, 1 ); memset( p, 0, sizeof(Extra_MmFlex_t) ); @@ -349,7 +319,7 @@ Extra_MmFlex_t * Extra_MmFlexStart() p->pCurrent = NULL; p->pEnd = NULL; - p->nChunkSize = (1 << 10); + p->nChunkSize = (1 << 12); p->nChunksAlloc = 64; p->nChunks = 0; p->pChunks = ALLOC( char *, p->nChunksAlloc ); @@ -370,31 +340,18 @@ Extra_MmFlex_t * Extra_MmFlexStart() SeeAlso [] ***********************************************************************/ -void Extra_MmFlexPrint( Extra_MmFlex_t * p ) -{ - printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n", - p->nChunkSize, p->nChunks ); - printf( " Entries used = %d. Memory used = %d. Memory alloc = %d.\n", - p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_MmFlexStop( Extra_MmFlex_t * p ) +void Extra_MmFlexStop( Extra_MmFlex_t * p, int fVerbose ) { int i; if ( p == NULL ) return; -//printf( "deleting flex\n" ); + if ( fVerbose ) + { + printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n", + p->nChunkSize, p->nChunks ); + printf( " Entries used = %d. Memory used = %d. Memory alloc = %d.\n", + p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc ); + } for ( i = 0; i < p->nChunks; i++ ) free( p->pChunks[i] ); free( p->pChunks ); @@ -491,7 +448,6 @@ Extra_MmStep_t * Extra_MmStepStart( int nSteps ) Extra_MmStep_t * p; int i, k; p = ALLOC( Extra_MmStep_t, 1 ); - memset( p, 0, sizeof(Extra_MmStep_t) ); p->nMems = nSteps; // start the fixed memory managers p->pMems = ALLOC( Extra_MmFixed_t *, p->nMems ); @@ -522,17 +478,11 @@ Extra_MmStep_t * Extra_MmStepStart( int nSteps ) SeeAlso [] ***********************************************************************/ -void Extra_MmStepStop( Extra_MmStep_t * p ) +void Extra_MmStepStop( Extra_MmStep_t * p, int fVerbose ) { int i; for ( i = 0; i < p->nMems; i++ ) - Extra_MmFixedStop( p->pMems[i] ); -// if ( p->pLargeChunks ) -// { -// for ( i = 0; i < p->nLargeChunks; i++ ) -// free( p->pLargeChunks[i] ); -// free( p->pLargeChunks ); -// } + Extra_MmFixedStop( p->pMems[i], fVerbose ); free( p->pMems ); free( p->pMap ); free( p ); @@ -556,17 +506,6 @@ char * Extra_MmStepEntryFetch( Extra_MmStep_t * p, int nBytes ) if ( nBytes > p->nMapSize ) { // printf( "Allocating %d bytes.\n", nBytes ); -/* - if ( p->nLargeChunks == p->nLargeChunksAlloc ) - { - if ( p->nLargeChunksAlloc == 0 ) - p->nLargeChunksAlloc = 5; - p->nLargeChunksAlloc *= 2; - p->pLargeChunks = REALLOC( char *, p->pLargeChunks, p->nLargeChunksAlloc ); - } - p->pLargeChunks[ p->nLargeChunks++ ] = ALLOC( char, nBytes ); - return p->pLargeChunks[ p->nLargeChunks - 1 ]; -*/ return ALLOC( char, nBytes ); } return Extra_MmFixedEntryFetch( p->pMap[nBytes] ); diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c index dff774bc..6d771990 100644 --- a/src/misc/extra/extraUtilMisc.c +++ b/src/misc/extra/extraUtilMisc.c @@ -209,37 +209,6 @@ int * Extra_DeriveRadixCode( int Number, int Radix, int nDigits ) return Code; } -/**Function************************************************************* - - Synopsis [Counts the number of ones in the bitstring.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Extra_CountOnes( unsigned char * pBytes, int nBytes ) -{ - static int bit_count[256] = { - 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5, - 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, - 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, - 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, - 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, - 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, - 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, - 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8 - }; - - int i, Counter; - Counter = 0; - for ( i = 0; i < nBytes; i++ ) - Counter += bit_count[ *(pBytes+i) ]; - return Counter; -} - /**Function******************************************************************** Synopsis [Computes the factorial.] @@ -1305,635 +1274,6 @@ void Extra_TruthPerm6One( unsigned * uTruth, int Phase, unsigned * uTruthRes ) /**Function************************************************************* - Synopsis [Computes a phase of the 8-var function.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_TruthExpand( int nVars, int nWords, unsigned * puTruth, unsigned uPhase, unsigned * puTruthR ) -{ - // elementary truth tables - static unsigned uTruths[8][8] = { - { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA }, - { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC }, - { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 }, - { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 }, - { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, - { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, - { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, - { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } - }; - static char Cases[256] = { - 0, // 00000000 - 0, // 00000001 - 1, // 00000010 - 0, // 00000011 - 2, // 00000100 - -1, // 00000101 - -1, // 00000110 - 0, // 00000111 - 3, // 00001000 - -1, // 00001001 - -1, // 00001010 - -1, // 00001011 - -1, // 00001100 - -1, // 00001101 - -1, // 00001110 - 0, // 00001111 - 4, // 00010000 - -1, // 00010001 - -1, // 00010010 - -1, // 00010011 - -1, // 00010100 - -1, // 00010101 - -1, // 00010110 - -1, // 00010111 - -1, // 00011000 - -1, // 00011001 - -1, // 00011010 - -1, // 00011011 - -1, // 00011100 - -1, // 00011101 - -1, // 00011110 - 0, // 00011111 - 5, // 00100000 - -1, // 00100001 - -1, // 00100010 - -1, // 00100011 - -1, // 00100100 - -1, // 00100101 - -1, // 00100110 - -1, // 00100111 - -1, // 00101000 - -1, // 00101001 - -1, // 00101010 - -1, // 00101011 - -1, // 00101100 - -1, // 00101101 - -1, // 00101110 - -1, // 00101111 - -1, // 00110000 - -1, // 00110001 - -1, // 00110010 - -1, // 00110011 - -1, // 00110100 - -1, // 00110101 - -1, // 00110110 - -1, // 00110111 - -1, // 00111000 - -1, // 00111001 - -1, // 00111010 - -1, // 00111011 - -1, // 00111100 - -1, // 00111101 - -1, // 00111110 - 0, // 00111111 - 6, // 01000000 - -1, // 01000001 - -1, // 01000010 - -1, // 01000011 - -1, // 01000100 - -1, // 01000101 - -1, // 01000110 - -1, // 01000111 - -1, // 01001000 - -1, // 01001001 - -1, // 01001010 - -1, // 01001011 - -1, // 01001100 - -1, // 01001101 - -1, // 01001110 - -1, // 01001111 - -1, // 01010000 - -1, // 01010001 - -1, // 01010010 - -1, // 01010011 - -1, // 01010100 - -1, // 01010101 - -1, // 01010110 - -1, // 01010111 - -1, // 01011000 - -1, // 01011001 - -1, // 01011010 - -1, // 01011011 - -1, // 01011100 - -1, // 01011101 - -1, // 01011110 - -1, // 01011111 - -1, // 01100000 - -1, // 01100001 - -1, // 01100010 - -1, // 01100011 - -1, // 01100100 - -1, // 01100101 - -1, // 01100110 - -1, // 01100111 - -1, // 01101000 - -1, // 01101001 - -1, // 01101010 - -1, // 01101011 - -1, // 01101100 - -1, // 01101101 - -1, // 01101110 - -1, // 01101111 - -1, // 01110000 - -1, // 01110001 - -1, // 01110010 - -1, // 01110011 - -1, // 01110100 - -1, // 01110101 - -1, // 01110110 - -1, // 01110111 - -1, // 01111000 - -1, // 01111001 - -1, // 01111010 - -1, // 01111011 - -1, // 01111100 - -1, // 01111101 - -1, // 01111110 - 0, // 01111111 - 7, // 10000000 - -1, // 10000001 - -1, // 10000010 - -1, // 10000011 - -1, // 10000100 - -1, // 10000101 - -1, // 10000110 - -1, // 10000111 - -1, // 10001000 - -1, // 10001001 - -1, // 10001010 - -1, // 10001011 - -1, // 10001100 - -1, // 10001101 - -1, // 10001110 - -1, // 10001111 - -1, // 10010000 - -1, // 10010001 - -1, // 10010010 - -1, // 10010011 - -1, // 10010100 - -1, // 10010101 - -1, // 10010110 - -1, // 10010111 - -1, // 10011000 - -1, // 10011001 - -1, // 10011010 - -1, // 10011011 - -1, // 10011100 - -1, // 10011101 - -1, // 10011110 - -1, // 10011111 - -1, // 10100000 - -1, // 10100001 - -1, // 10100010 - -1, // 10100011 - -1, // 10100100 - -1, // 10100101 - -1, // 10100110 - -1, // 10100111 - -1, // 10101000 - -1, // 10101001 - -1, // 10101010 - -1, // 10101011 - -1, // 10101100 - -1, // 10101101 - -1, // 10101110 - -1, // 10101111 - -1, // 10110000 - -1, // 10110001 - -1, // 10110010 - -1, // 10110011 - -1, // 10110100 - -1, // 10110101 - -1, // 10110110 - -1, // 10110111 - -1, // 10111000 - -1, // 10111001 - -1, // 10111010 - -1, // 10111011 - -1, // 10111100 - -1, // 10111101 - -1, // 10111110 - -1, // 10111111 - -1, // 11000000 - -1, // 11000001 - -1, // 11000010 - -1, // 11000011 - -1, // 11000100 - -1, // 11000101 - -1, // 11000110 - -1, // 11000111 - -1, // 11001000 - -1, // 11001001 - -1, // 11001010 - -1, // 11001011 - -1, // 11001100 - -1, // 11001101 - -1, // 11001110 - -1, // 11001111 - -1, // 11010000 - -1, // 11010001 - -1, // 11010010 - -1, // 11010011 - -1, // 11010100 - -1, // 11010101 - -1, // 11010110 - -1, // 11010111 - -1, // 11011000 - -1, // 11011001 - -1, // 11011010 - -1, // 11011011 - -1, // 11011100 - -1, // 11011101 - -1, // 11011110 - -1, // 11011111 - -1, // 11100000 - -1, // 11100001 - -1, // 11100010 - -1, // 11100011 - -1, // 11100100 - -1, // 11100101 - -1, // 11100110 - -1, // 11100111 - -1, // 11101000 - -1, // 11101001 - -1, // 11101010 - -1, // 11101011 - -1, // 11101100 - -1, // 11101101 - -1, // 11101110 - -1, // 11101111 - -1, // 11110000 - -1, // 11110001 - -1, // 11110010 - -1, // 11110011 - -1, // 11110100 - -1, // 11110101 - -1, // 11110110 - -1, // 11110111 - -1, // 11111000 - -1, // 11111001 - -1, // 11111010 - -1, // 11111011 - -1, // 11111100 - -1, // 11111101 - -1, // 11111110 - 0 // 11111111 - }; - static char Perms[256][8] = { - { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00000000 - { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00000001 - { 1, 0, 2, 3, 4, 5, 6, 7 }, // 00000010 - { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00000011 - { 1, 2, 0, 3, 4, 5, 6, 7 }, // 00000100 - { 0, 2, 1, 3, 4, 5, 6, 7 }, // 00000101 - { 2, 0, 1, 3, 4, 5, 6, 7 }, // 00000110 - { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00000111 - { 1, 2, 3, 0, 4, 5, 6, 7 }, // 00001000 - { 0, 2, 3, 1, 4, 5, 6, 7 }, // 00001001 - { 2, 0, 3, 1, 4, 5, 6, 7 }, // 00001010 - { 0, 1, 3, 2, 4, 5, 6, 7 }, // 00001011 - { 2, 3, 0, 1, 4, 5, 6, 7 }, // 00001100 - { 0, 3, 1, 2, 4, 5, 6, 7 }, // 00001101 - { 3, 0, 1, 2, 4, 5, 6, 7 }, // 00001110 - { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00001111 - { 1, 2, 3, 4, 0, 5, 6, 7 }, // 00010000 - { 0, 2, 3, 4, 1, 5, 6, 7 }, // 00010001 - { 2, 0, 3, 4, 1, 5, 6, 7 }, // 00010010 - { 0, 1, 3, 4, 2, 5, 6, 7 }, // 00010011 - { 2, 3, 0, 4, 1, 5, 6, 7 }, // 00010100 - { 0, 3, 1, 4, 2, 5, 6, 7 }, // 00010101 - { 3, 0, 1, 4, 2, 5, 6, 7 }, // 00010110 - { 0, 1, 2, 4, 3, 5, 6, 7 }, // 00010111 - { 2, 3, 4, 0, 1, 5, 6, 7 }, // 00011000 - { 0, 3, 4, 1, 2, 5, 6, 7 }, // 00011001 - { 3, 0, 4, 1, 2, 5, 6, 7 }, // 00011010 - { 0, 1, 4, 2, 3, 5, 6, 7 }, // 00011011 - { 3, 4, 0, 1, 2, 5, 6, 7 }, // 00011100 - { 0, 4, 1, 2, 3, 5, 6, 7 }, // 00011101 - { 4, 0, 1, 2, 3, 5, 6, 7 }, // 00011110 - { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00011111 - { 1, 2, 3, 4, 5, 0, 6, 7 }, // 00100000 - { 0, 2, 3, 4, 5, 1, 6, 7 }, // 00100001 - { 2, 0, 3, 4, 5, 1, 6, 7 }, // 00100010 - { 0, 1, 3, 4, 5, 2, 6, 7 }, // 00100011 - { 2, 3, 0, 4, 5, 1, 6, 7 }, // 00100100 - { 0, 3, 1, 4, 5, 2, 6, 7 }, // 00100101 - { 3, 0, 1, 4, 5, 2, 6, 7 }, // 00100110 - { 0, 1, 2, 4, 5, 3, 6, 7 }, // 00100111 - { 2, 3, 4, 0, 5, 1, 6, 7 }, // 00101000 - { 0, 3, 4, 1, 5, 2, 6, 7 }, // 00101001 - { 3, 0, 4, 1, 5, 2, 6, 7 }, // 00101010 - { 0, 1, 4, 2, 5, 3, 6, 7 }, // 00101011 - { 3, 4, 0, 1, 5, 2, 6, 7 }, // 00101100 - { 0, 4, 1, 2, 5, 3, 6, 7 }, // 00101101 - { 4, 0, 1, 2, 5, 3, 6, 7 }, // 00101110 - { 0, 1, 2, 3, 5, 4, 6, 7 }, // 00101111 - { 2, 3, 4, 5, 0, 1, 6, 7 }, // 00110000 - { 0, 3, 4, 5, 1, 2, 6, 7 }, // 00110001 - { 3, 0, 4, 5, 1, 2, 6, 7 }, // 00110010 - { 0, 1, 4, 5, 2, 3, 6, 7 }, // 00110011 - { 3, 4, 0, 5, 1, 2, 6, 7 }, // 00110100 - { 0, 4, 1, 5, 2, 3, 6, 7 }, // 00110101 - { 4, 0, 1, 5, 2, 3, 6, 7 }, // 00110110 - { 0, 1, 2, 5, 3, 4, 6, 7 }, // 00110111 - { 3, 4, 5, 0, 1, 2, 6, 7 }, // 00111000 - { 0, 4, 5, 1, 2, 3, 6, 7 }, // 00111001 - { 4, 0, 5, 1, 2, 3, 6, 7 }, // 00111010 - { 0, 1, 5, 2, 3, 4, 6, 7 }, // 00111011 - { 4, 5, 0, 1, 2, 3, 6, 7 }, // 00111100 - { 0, 5, 1, 2, 3, 4, 6, 7 }, // 00111101 - { 5, 0, 1, 2, 3, 4, 6, 7 }, // 00111110 - { 0, 1, 2, 3, 4, 5, 6, 7 }, // 00111111 - { 1, 2, 3, 4, 5, 6, 0, 7 }, // 01000000 - { 0, 2, 3, 4, 5, 6, 1, 7 }, // 01000001 - { 2, 0, 3, 4, 5, 6, 1, 7 }, // 01000010 - { 0, 1, 3, 4, 5, 6, 2, 7 }, // 01000011 - { 2, 3, 0, 4, 5, 6, 1, 7 }, // 01000100 - { 0, 3, 1, 4, 5, 6, 2, 7 }, // 01000101 - { 3, 0, 1, 4, 5, 6, 2, 7 }, // 01000110 - { 0, 1, 2, 4, 5, 6, 3, 7 }, // 01000111 - { 2, 3, 4, 0, 5, 6, 1, 7 }, // 01001000 - { 0, 3, 4, 1, 5, 6, 2, 7 }, // 01001001 - { 3, 0, 4, 1, 5, 6, 2, 7 }, // 01001010 - { 0, 1, 4, 2, 5, 6, 3, 7 }, // 01001011 - { 3, 4, 0, 1, 5, 6, 2, 7 }, // 01001100 - { 0, 4, 1, 2, 5, 6, 3, 7 }, // 01001101 - { 4, 0, 1, 2, 5, 6, 3, 7 }, // 01001110 - { 0, 1, 2, 3, 5, 6, 4, 7 }, // 01001111 - { 2, 3, 4, 5, 0, 6, 1, 7 }, // 01010000 - { 0, 3, 4, 5, 1, 6, 2, 7 }, // 01010001 - { 3, 0, 4, 5, 1, 6, 2, 7 }, // 01010010 - { 0, 1, 4, 5, 2, 6, 3, 7 }, // 01010011 - { 3, 4, 0, 5, 1, 6, 2, 7 }, // 01010100 - { 0, 4, 1, 5, 2, 6, 3, 7 }, // 01010101 - { 4, 0, 1, 5, 2, 6, 3, 7 }, // 01010110 - { 0, 1, 2, 5, 3, 6, 4, 7 }, // 01010111 - { 3, 4, 5, 0, 1, 6, 2, 7 }, // 01011000 - { 0, 4, 5, 1, 2, 6, 3, 7 }, // 01011001 - { 4, 0, 5, 1, 2, 6, 3, 7 }, // 01011010 - { 0, 1, 5, 2, 3, 6, 4, 7 }, // 01011011 - { 4, 5, 0, 1, 2, 6, 3, 7 }, // 01011100 - { 0, 5, 1, 2, 3, 6, 4, 7 }, // 01011101 - { 5, 0, 1, 2, 3, 6, 4, 7 }, // 01011110 - { 0, 1, 2, 3, 4, 6, 5, 7 }, // 01011111 - { 2, 3, 4, 5, 6, 0, 1, 7 }, // 01100000 - { 0, 3, 4, 5, 6, 1, 2, 7 }, // 01100001 - { 3, 0, 4, 5, 6, 1, 2, 7 }, // 01100010 - { 0, 1, 4, 5, 6, 2, 3, 7 }, // 01100011 - { 3, 4, 0, 5, 6, 1, 2, 7 }, // 01100100 - { 0, 4, 1, 5, 6, 2, 3, 7 }, // 01100101 - { 4, 0, 1, 5, 6, 2, 3, 7 }, // 01100110 - { 0, 1, 2, 5, 6, 3, 4, 7 }, // 01100111 - { 3, 4, 5, 0, 6, 1, 2, 7 }, // 01101000 - { 0, 4, 5, 1, 6, 2, 3, 7 }, // 01101001 - { 4, 0, 5, 1, 6, 2, 3, 7 }, // 01101010 - { 0, 1, 5, 2, 6, 3, 4, 7 }, // 01101011 - { 4, 5, 0, 1, 6, 2, 3, 7 }, // 01101100 - { 0, 5, 1, 2, 6, 3, 4, 7 }, // 01101101 - { 5, 0, 1, 2, 6, 3, 4, 7 }, // 01101110 - { 0, 1, 2, 3, 6, 4, 5, 7 }, // 01101111 - { 3, 4, 5, 6, 0, 1, 2, 7 }, // 01110000 - { 0, 4, 5, 6, 1, 2, 3, 7 }, // 01110001 - { 4, 0, 5, 6, 1, 2, 3, 7 }, // 01110010 - { 0, 1, 5, 6, 2, 3, 4, 7 }, // 01110011 - { 4, 5, 0, 6, 1, 2, 3, 7 }, // 01110100 - { 0, 5, 1, 6, 2, 3, 4, 7 }, // 01110101 - { 5, 0, 1, 6, 2, 3, 4, 7 }, // 01110110 - { 0, 1, 2, 6, 3, 4, 5, 7 }, // 01110111 - { 4, 5, 6, 0, 1, 2, 3, 7 }, // 01111000 - { 0, 5, 6, 1, 2, 3, 4, 7 }, // 01111001 - { 5, 0, 6, 1, 2, 3, 4, 7 }, // 01111010 - { 0, 1, 6, 2, 3, 4, 5, 7 }, // 01111011 - { 5, 6, 0, 1, 2, 3, 4, 7 }, // 01111100 - { 0, 6, 1, 2, 3, 4, 5, 7 }, // 01111101 - { 6, 0, 1, 2, 3, 4, 5, 7 }, // 01111110 - { 0, 1, 2, 3, 4, 5, 6, 7 }, // 01111111 - { 1, 2, 3, 4, 5, 6, 7, 0 }, // 10000000 - { 0, 2, 3, 4, 5, 6, 7, 1 }, // 10000001 - { 2, 0, 3, 4, 5, 6, 7, 1 }, // 10000010 - { 0, 1, 3, 4, 5, 6, 7, 2 }, // 10000011 - { 2, 3, 0, 4, 5, 6, 7, 1 }, // 10000100 - { 0, 3, 1, 4, 5, 6, 7, 2 }, // 10000101 - { 3, 0, 1, 4, 5, 6, 7, 2 }, // 10000110 - { 0, 1, 2, 4, 5, 6, 7, 3 }, // 10000111 - { 2, 3, 4, 0, 5, 6, 7, 1 }, // 10001000 - { 0, 3, 4, 1, 5, 6, 7, 2 }, // 10001001 - { 3, 0, 4, 1, 5, 6, 7, 2 }, // 10001010 - { 0, 1, 4, 2, 5, 6, 7, 3 }, // 10001011 - { 3, 4, 0, 1, 5, 6, 7, 2 }, // 10001100 - { 0, 4, 1, 2, 5, 6, 7, 3 }, // 10001101 - { 4, 0, 1, 2, 5, 6, 7, 3 }, // 10001110 - { 0, 1, 2, 3, 5, 6, 7, 4 }, // 10001111 - { 2, 3, 4, 5, 0, 6, 7, 1 }, // 10010000 - { 0, 3, 4, 5, 1, 6, 7, 2 }, // 10010001 - { 3, 0, 4, 5, 1, 6, 7, 2 }, // 10010010 - { 0, 1, 4, 5, 2, 6, 7, 3 }, // 10010011 - { 3, 4, 0, 5, 1, 6, 7, 2 }, // 10010100 - { 0, 4, 1, 5, 2, 6, 7, 3 }, // 10010101 - { 4, 0, 1, 5, 2, 6, 7, 3 }, // 10010110 - { 0, 1, 2, 5, 3, 6, 7, 4 }, // 10010111 - { 3, 4, 5, 0, 1, 6, 7, 2 }, // 10011000 - { 0, 4, 5, 1, 2, 6, 7, 3 }, // 10011001 - { 4, 0, 5, 1, 2, 6, 7, 3 }, // 10011010 - { 0, 1, 5, 2, 3, 6, 7, 4 }, // 10011011 - { 4, 5, 0, 1, 2, 6, 7, 3 }, // 10011100 - { 0, 5, 1, 2, 3, 6, 7, 4 }, // 10011101 - { 5, 0, 1, 2, 3, 6, 7, 4 }, // 10011110 - { 0, 1, 2, 3, 4, 6, 7, 5 }, // 10011111 - { 2, 3, 4, 5, 6, 0, 7, 1 }, // 10100000 - { 0, 3, 4, 5, 6, 1, 7, 2 }, // 10100001 - { 3, 0, 4, 5, 6, 1, 7, 2 }, // 10100010 - { 0, 1, 4, 5, 6, 2, 7, 3 }, // 10100011 - { 3, 4, 0, 5, 6, 1, 7, 2 }, // 10100100 - { 0, 4, 1, 5, 6, 2, 7, 3 }, // 10100101 - { 4, 0, 1, 5, 6, 2, 7, 3 }, // 10100110 - { 0, 1, 2, 5, 6, 3, 7, 4 }, // 10100111 - { 3, 4, 5, 0, 6, 1, 7, 2 }, // 10101000 - { 0, 4, 5, 1, 6, 2, 7, 3 }, // 10101001 - { 4, 0, 5, 1, 6, 2, 7, 3 }, // 10101010 - { 0, 1, 5, 2, 6, 3, 7, 4 }, // 10101011 - { 4, 5, 0, 1, 6, 2, 7, 3 }, // 10101100 - { 0, 5, 1, 2, 6, 3, 7, 4 }, // 10101101 - { 5, 0, 1, 2, 6, 3, 7, 4 }, // 10101110 - { 0, 1, 2, 3, 6, 4, 7, 5 }, // 10101111 - { 3, 4, 5, 6, 0, 1, 7, 2 }, // 10110000 - { 0, 4, 5, 6, 1, 2, 7, 3 }, // 10110001 - { 4, 0, 5, 6, 1, 2, 7, 3 }, // 10110010 - { 0, 1, 5, 6, 2, 3, 7, 4 }, // 10110011 - { 4, 5, 0, 6, 1, 2, 7, 3 }, // 10110100 - { 0, 5, 1, 6, 2, 3, 7, 4 }, // 10110101 - { 5, 0, 1, 6, 2, 3, 7, 4 }, // 10110110 - { 0, 1, 2, 6, 3, 4, 7, 5 }, // 10110111 - { 4, 5, 6, 0, 1, 2, 7, 3 }, // 10111000 - { 0, 5, 6, 1, 2, 3, 7, 4 }, // 10111001 - { 5, 0, 6, 1, 2, 3, 7, 4 }, // 10111010 - { 0, 1, 6, 2, 3, 4, 7, 5 }, // 10111011 - { 5, 6, 0, 1, 2, 3, 7, 4 }, // 10111100 - { 0, 6, 1, 2, 3, 4, 7, 5 }, // 10111101 - { 6, 0, 1, 2, 3, 4, 7, 5 }, // 10111110 - { 0, 1, 2, 3, 4, 5, 7, 6 }, // 10111111 - { 2, 3, 4, 5, 6, 7, 0, 1 }, // 11000000 - { 0, 3, 4, 5, 6, 7, 1, 2 }, // 11000001 - { 3, 0, 4, 5, 6, 7, 1, 2 }, // 11000010 - { 0, 1, 4, 5, 6, 7, 2, 3 }, // 11000011 - { 3, 4, 0, 5, 6, 7, 1, 2 }, // 11000100 - { 0, 4, 1, 5, 6, 7, 2, 3 }, // 11000101 - { 4, 0, 1, 5, 6, 7, 2, 3 }, // 11000110 - { 0, 1, 2, 5, 6, 7, 3, 4 }, // 11000111 - { 3, 4, 5, 0, 6, 7, 1, 2 }, // 11001000 - { 0, 4, 5, 1, 6, 7, 2, 3 }, // 11001001 - { 4, 0, 5, 1, 6, 7, 2, 3 }, // 11001010 - { 0, 1, 5, 2, 6, 7, 3, 4 }, // 11001011 - { 4, 5, 0, 1, 6, 7, 2, 3 }, // 11001100 - { 0, 5, 1, 2, 6, 7, 3, 4 }, // 11001101 - { 5, 0, 1, 2, 6, 7, 3, 4 }, // 11001110 - { 0, 1, 2, 3, 6, 7, 4, 5 }, // 11001111 - { 3, 4, 5, 6, 0, 7, 1, 2 }, // 11010000 - { 0, 4, 5, 6, 1, 7, 2, 3 }, // 11010001 - { 4, 0, 5, 6, 1, 7, 2, 3 }, // 11010010 - { 0, 1, 5, 6, 2, 7, 3, 4 }, // 11010011 - { 4, 5, 0, 6, 1, 7, 2, 3 }, // 11010100 - { 0, 5, 1, 6, 2, 7, 3, 4 }, // 11010101 - { 5, 0, 1, 6, 2, 7, 3, 4 }, // 11010110 - { 0, 1, 2, 6, 3, 7, 4, 5 }, // 11010111 - { 4, 5, 6, 0, 1, 7, 2, 3 }, // 11011000 - { 0, 5, 6, 1, 2, 7, 3, 4 }, // 11011001 - { 5, 0, 6, 1, 2, 7, 3, 4 }, // 11011010 - { 0, 1, 6, 2, 3, 7, 4, 5 }, // 11011011 - { 5, 6, 0, 1, 2, 7, 3, 4 }, // 11011100 - { 0, 6, 1, 2, 3, 7, 4, 5 }, // 11011101 - { 6, 0, 1, 2, 3, 7, 4, 5 }, // 11011110 - { 0, 1, 2, 3, 4, 7, 5, 6 }, // 11011111 - { 3, 4, 5, 6, 7, 0, 1, 2 }, // 11100000 - { 0, 4, 5, 6, 7, 1, 2, 3 }, // 11100001 - { 4, 0, 5, 6, 7, 1, 2, 3 }, // 11100010 - { 0, 1, 5, 6, 7, 2, 3, 4 }, // 11100011 - { 4, 5, 0, 6, 7, 1, 2, 3 }, // 11100100 - { 0, 5, 1, 6, 7, 2, 3, 4 }, // 11100101 - { 5, 0, 1, 6, 7, 2, 3, 4 }, // 11100110 - { 0, 1, 2, 6, 7, 3, 4, 5 }, // 11100111 - { 4, 5, 6, 0, 7, 1, 2, 3 }, // 11101000 - { 0, 5, 6, 1, 7, 2, 3, 4 }, // 11101001 - { 5, 0, 6, 1, 7, 2, 3, 4 }, // 11101010 - { 0, 1, 6, 2, 7, 3, 4, 5 }, // 11101011 - { 5, 6, 0, 1, 7, 2, 3, 4 }, // 11101100 - { 0, 6, 1, 2, 7, 3, 4, 5 }, // 11101101 - { 6, 0, 1, 2, 7, 3, 4, 5 }, // 11101110 - { 0, 1, 2, 3, 7, 4, 5, 6 }, // 11101111 - { 4, 5, 6, 7, 0, 1, 2, 3 }, // 11110000 - { 0, 5, 6, 7, 1, 2, 3, 4 }, // 11110001 - { 5, 0, 6, 7, 1, 2, 3, 4 }, // 11110010 - { 0, 1, 6, 7, 2, 3, 4, 5 }, // 11110011 - { 5, 6, 0, 7, 1, 2, 3, 4 }, // 11110100 - { 0, 6, 1, 7, 2, 3, 4, 5 }, // 11110101 - { 6, 0, 1, 7, 2, 3, 4, 5 }, // 11110110 - { 0, 1, 2, 7, 3, 4, 5, 6 }, // 11110111 - { 5, 6, 7, 0, 1, 2, 3, 4 }, // 11111000 - { 0, 6, 7, 1, 2, 3, 4, 5 }, // 11111001 - { 6, 0, 7, 1, 2, 3, 4, 5 }, // 11111010 - { 0, 1, 7, 2, 3, 4, 5, 6 }, // 11111011 - { 6, 7, 0, 1, 2, 3, 4, 5 }, // 11111100 - { 0, 7, 1, 2, 3, 4, 5, 6 }, // 11111101 - { 7, 0, 1, 2, 3, 4, 5, 6 }, // 11111110 - { 0, 1, 2, 3, 4, 5, 6, 7 } // 11111111 - }; - - assert( uPhase > 0 && uPhase < (unsigned)(1 << nVars) ); - - // the same function - if ( Cases[uPhase] == 0 ) - { - int i; - for ( i = 0; i < nWords; i++ ) - puTruthR[i] = puTruth[i]; - return; - } - - // an elementary variable - if ( Cases[uPhase] > 0 ) - { - int i; - for ( i = 0; i < nWords; i++ ) - puTruthR[i] = uTruths[Cases[uPhase]][i]; - return; - } - - // truth table takes one word - if ( nWords == 1 ) - { - int i, k, nMints, iRes; - char * pPerm = Perms[uPhase]; - puTruthR[0] = 0; - nMints = (1 << nVars); - for ( i = 0; i < nMints; i++ ) - if ( puTruth[0] & (1 << i) ) - { - for ( iRes = 0, k = 0; k < nVars; k++ ) - if ( i & (1 << pPerm[k]) ) - iRes |= (1 << k); - puTruthR[0] |= (1 << iRes); - } - return; - } - else if ( nWords == 2 ) - { - int i, k, iRes; - char * pPerm = Perms[uPhase]; - puTruthR[0] = puTruthR[1] = 0; - for ( i = 0; i < 32; i++ ) - { - if ( puTruth[0] & (1 << i) ) - { - for ( iRes = 0, k = 0; k < 6; k++ ) - if ( i & (1 << pPerm[k]) ) - iRes |= (1 << k); - if ( iRes < 32 ) - puTruthR[0] |= (1 << iRes); - else - puTruthR[1] |= (1 << (iRes-32)); - } - } - for ( ; i < 64; i++ ) - { - if ( puTruth[1] & (1 << (i-32)) ) - { - for ( iRes = 0, k = 0; k < 6; k++ ) - if ( i & (1 << pPerm[k]) ) - iRes |= (1 << k); - if ( iRes < 32 ) - puTruthR[0] |= (1 << iRes); - else - puTruthR[1] |= (1 << (iRes-32)); - } - } - } - // truth table takes more than one word - else - { - int i, k, nMints, iRes; - char * pPerm = Perms[uPhase]; - for ( i = 0; i < nWords; i++ ) - puTruthR[i] = 0; - nMints = (1 << nVars); - for ( i = 0; i < nMints; i++ ) - if ( puTruth[i>>5] & (1 << (i&31)) ) - { - for ( iRes = 0, k = 0; k < 5; k++ ) - if ( i & (1 << pPerm[k]) ) - iRes |= (1 << k); - puTruthR[iRes>>5] |= (1 << (iRes&31)); - } - } -} - -/**Function************************************************************* - Synopsis [Allocated lookup table for truth table permutation.] Description [] @@ -2041,84 +1381,6 @@ unsigned ** Extra_TruthPerm63() /**Function************************************************************* - Synopsis [Returns the pointer to the elementary truth tables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned ** Extra_Truths8() -{ - static unsigned uTruths[8][8] = { - { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA }, - { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC }, - { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 }, - { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 }, - { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, - { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, - { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, - { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } - }; - static unsigned * puResult[8] = { - uTruths[0], uTruths[1], uTruths[2], uTruths[3], uTruths[4], uTruths[5], uTruths[6], uTruths[7] - }; - return (unsigned **)puResult; -} - -/**Function************************************************************* - - Synopsis [Bubble-sorts components by scores in increasing order.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_BubbleSort( int Order[], int Costs[], int nSize, int fIncreasing ) -{ - int i, Temp, fChanges; - assert( nSize < 1000 ); - for ( i = 0; i < nSize; i++ ) - Order[i] = i; - if ( fIncreasing ) - { - do { - fChanges = 0; - for ( i = 0; i < nSize - 1; i++ ) - { - if ( Costs[Order[i]] <= Costs[Order[i+1]] ) - continue; - Temp = Order[i]; - Order[i] = Order[i+1]; - Order[i+1] = Temp; - fChanges = 1; - } - } while ( fChanges ); - } - else - { - do { - fChanges = 0; - for ( i = 0; i < nSize - 1; i++ ) - { - if ( Costs[Order[i]] >= Costs[Order[i+1]] ) - continue; - Temp = Order[i]; - Order[i] = Order[i+1]; - Order[i+1] = Temp; - fChanges = 1; - } - } while ( fChanges ); - } -} - -/**Function************************************************************* - Synopsis [Returns the smallest prime larger than the number.] Description [] @@ -2153,6 +1415,7 @@ unsigned int Cudd_PrimeCopy( unsigned int p) } /* end of Cudd_Prime */ + /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ @@ -2162,72 +1425,6 @@ unsigned int Cudd_PrimeCopy( unsigned int p) /*---------------------------------------------------------------------------*/ -/**Function************************************************************* - - Synopsis [Computes the permutation table for 8 variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_TruthExpandGeneratePermTable() -{ - int i, k, nOnes, Last1, First0; - int iOne, iZero; - - printf( "\nstatic char Cases[256] = {\n" ); - for ( i = 0; i < 256; i++ ) - { - nOnes = 0; - Last1 = First0 = -1; - for ( k = 0; k < 8; k++ ) - { - if ( i & (1 << k) ) - { - nOnes++; - Last1 = k; - } - else if ( First0 == -1 ) - First0 = k; - } - if ( Last1 + 1 == First0 || i == 255 ) - printf( " %d%s", 0, (i==255? " ":",") ); - else if ( nOnes == 1 ) - printf( " %d,", Last1 ); - else - printf( " -%d,", 1 ); - printf( " // " ); - Extra_PrintBinary( stdout, (unsigned*)&i, 8 ); - printf( "\n" ); - } - printf( "};\n" ); - - printf( "\nstatic char Perms[256][8] = {\n" ); - for ( i = 0; i < 256; i++ ) - { - printf( " {" ); - nOnes = 0; - for ( k = 0; k < 8; k++ ) - if ( i & (1 << k) ) - nOnes++; - iOne = 0; - iZero = nOnes; - for ( k = 0; k < 8; k++ ) - if ( i & (1 << k) ) - printf( "%s %d", (k==0? "":","), iOne++ ); - else - printf( "%s %d", (k==0? "":","), iZero++ ); - assert( iOne + iZero == 8 ); - printf( " }%s // ", (i==255? " ":",") ); - Extra_PrintBinary( stdout, (unsigned*)&i, 8 ); - printf( "\n" ); - } - printf( "};\n" ); -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/extra/extraUtilProgress.c b/src/misc/extra/extraUtilProgress.c index 6b6d5132..7b0efb5c 100644 --- a/src/misc/extra/extraUtilProgress.c +++ b/src/misc/extra/extraUtilProgress.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include <stdio.h> +#include "stdio.h" #include "extra.h" //////////////////////////////////////////////////////////////////////// @@ -38,7 +38,7 @@ static void Extra_ProgressBarShow( ProgressBar * p, char * pString ); static void Extra_ProgressBarClean( ProgressBar * p ); //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// +/// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -58,17 +58,13 @@ static void Extra_ProgressBarClean( ProgressBar * p ); ProgressBar * Extra_ProgressBarStart( FILE * pFile, int nItemsTotal ) { ProgressBar * p; - extern int Abc_FrameShowProgress( void * p ); - extern void * Abc_FrameGetGlobalFrame(); - - if ( !Abc_FrameShowProgress(Abc_FrameGetGlobalFrame()) ) return NULL; p = ALLOC( ProgressBar, 1 ); memset( p, 0, sizeof(ProgressBar) ); p->pFile = pFile; p->nItemsTotal = nItemsTotal; p->posTotal = 78; p->posCur = 1; - p->nItemsNext = (int)((7.0+p->posCur)*p->nItemsTotal/p->posTotal); + p->nItemsNext = (int)((float)p->nItemsTotal/p->posTotal)*(p->posCur+5)+2; Extra_ProgressBarShow( p, NULL ); return p; } @@ -86,19 +82,14 @@ ProgressBar * Extra_ProgressBarStart( FILE * pFile, int nItemsTotal ) ***********************************************************************/ void Extra_ProgressBarUpdate_int( ProgressBar * p, int nItemsCur, char * pString ) { - if ( p == NULL ) return; if ( nItemsCur < p->nItemsNext ) return; - if ( nItemsCur >= p->nItemsTotal ) - { - p->posCur = 78; - p->nItemsNext = 0x7FFFFFFF; - } - else - { - p->posCur += 7; - p->nItemsNext = (int)((7.0+p->posCur)*p->nItemsTotal/p->posTotal); - } + if ( nItemsCur > p->nItemsTotal ) + nItemsCur = p->nItemsTotal; + p->posCur = (int)((float)nItemsCur * p->posTotal / p->nItemsTotal); + p->nItemsNext = (int)((float)p->nItemsTotal/p->posTotal)*(p->posCur+10)+1; + if ( p->posCur == 0 ) + p->posCur = 1; Extra_ProgressBarShow( p, pString ); } @@ -116,7 +107,6 @@ void Extra_ProgressBarUpdate_int( ProgressBar * p, int nItemsCur, char * pString ***********************************************************************/ void Extra_ProgressBarStop( ProgressBar * p ) { - if ( p == NULL ) return; Extra_ProgressBarClean( p ); FREE( p ); } @@ -135,7 +125,6 @@ void Extra_ProgressBarStop( ProgressBar * p ) void Extra_ProgressBarShow( ProgressBar * p, char * pString ) { int i; - if ( p == NULL ) return; if ( pString ) fprintf( p->pFile, "%s ", pString ); for ( i = (pString? strlen(pString) + 1 : 0); i < p->posCur; i++ ) @@ -162,7 +151,6 @@ void Extra_ProgressBarShow( ProgressBar * p, char * pString ) void Extra_ProgressBarClean( ProgressBar * p ) { int i; - if ( p == NULL ) return; for ( i = 0; i <= p->posTotal; i++ ) fprintf( p->pFile, " " ); fprintf( p->pFile, "\r" ); diff --git a/src/misc/extra/extraUtilReader.c b/src/misc/extra/extraUtilReader.c index c165b989..042dfaca 100644 --- a/src/misc/extra/extraUtilReader.c +++ b/src/misc/extra/extraUtilReader.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include <stdio.h> +#include "stdio.h" #include "extra.h" #include "vec.h" @@ -26,7 +26,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define EXTRA_BUFFER_SIZE 4*1048576 // 1M - size of the data chunk stored in memory +#define EXTRA_BUFFER_SIZE 1048576 // 1M - size of the data chunk stored in memory #define EXTRA_OFFSET_SIZE 4096 // 4K - load new data when less than this is left #define EXTRA_MINIMUM(a,b) (((a) < (b))? (a) : (b)) @@ -67,7 +67,7 @@ static void * Extra_FileReaderGetTokens_int( Extra_FileReader_t * p ); static void Extra_FileReaderReload( Extra_FileReader_t * p ); //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// +/// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -262,9 +262,6 @@ void * Extra_FileReaderGetTokens_int( Extra_FileReader_t * p ) // check if the new data should to be loaded if ( p->pBufferCur > p->pBufferStop ) Extra_FileReaderReload( p ); - -// printf( "%d\n", p->pBufferEnd - p->pBufferCur ); - // process the string starting from the current position for ( pChar = p->pBufferCur; pChar < p->pBufferEnd; pChar++ ) { @@ -273,10 +270,6 @@ void * Extra_FileReaderGetTokens_int( Extra_FileReader_t * p ) p->nLineCounter++; // switch depending on the character MapValue = p->pCharMap[*pChar]; - -// printf( "Char value = %d. Map value = %d.\n", *pChar, MapValue ); - - switch ( MapValue ) { case EXTRA_CHAR_COMMENT: @@ -333,14 +326,6 @@ void * Extra_FileReaderGetTokens_int( Extra_FileReader_t * p ) return p->vTokens; } printf( "Extra_FileReader failed to parse the file \"%s\".\n", p->pFileName ); -/* - { - int i; - for ( i = 0; i < p->vTokens->nSize; i++ ) - printf( "%s ", p->vTokens->pArray[i] ); - printf( "\n" ); - } -*/ return NULL; } diff --git a/src/misc/extra/extraUtilTruth.c b/src/misc/extra/extraUtilTruth.c deleted file mode 100644 index 3b0b16eb..00000000 --- a/src/misc/extra/extraUtilTruth.c +++ /dev/null @@ -1,1148 +0,0 @@ -/**CFile**************************************************************** - - FileName [extraUtilMisc.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [extra] - - Synopsis [Various procedures for truth table manipulation.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: extraUtilMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "extra.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -static unsigned s_VarMasks[5][2] = { - { 0x33333333, 0xAAAAAAAA }, - { 0x55555555, 0xCCCCCCCC }, - { 0x0F0F0F0F, 0xF0F0F0F0 }, - { 0x00FF00FF, 0xFF00FF00 }, - { 0x0000FFFF, 0xFFFF0000 } -}; - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -/**AutomaticEnd***************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - -/**Function************************************************************* - - Synopsis [Derive elementary truth tables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned ** Extra_TruthElementary( int nVars ) -{ - unsigned ** pRes; - int i, k, nWords; - nWords = Extra_TruthWordNum(nVars); - pRes = (unsigned **)Extra_ArrayAlloc( nVars, nWords, 4 ); - for ( i = 0; i < nVars; i++ ) - { - if ( i < 5 ) - { - for ( k = 0; k < nWords; k++ ) - pRes[i][k] = s_VarMasks[i][1]; - } - else - { - for ( k = 0; k < nWords; k++ ) - if ( k & (1 << (i-5)) ) - pRes[i][k] = ~(unsigned)0; - else - pRes[i][k] = 0; - } - } - return pRes; -} - -/**Function************************************************************* - - Synopsis [Swaps two adjacent variables in the truth table.] - - Description [Swaps var number Start and var number Start+1 (0-based numbers). - The input truth table is pIn. The output truth table is pOut.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int iVar ) -{ - static unsigned PMasks[4][3] = { - { 0x99999999, 0x22222222, 0x44444444 }, - { 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 }, - { 0xF00FF00F, 0x00F000F0, 0x0F000F00 }, - { 0xFF0000FF, 0x0000FF00, 0x00FF0000 } - }; - int nWords = Extra_TruthWordNum( nVars ); - int i, k, Step, Shift; - - assert( iVar < nVars - 1 ); - if ( iVar < 4 ) - { - Shift = (1 << iVar); - for ( i = 0; i < nWords; i++ ) - pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift); - } - else if ( iVar > 4 ) - { - Step = (1 << (iVar - 5)); - for ( k = 0; k < nWords; k += 4*Step ) - { - for ( i = 0; i < Step; i++ ) - pOut[i] = pIn[i]; - for ( i = 0; i < Step; i++ ) - pOut[Step+i] = pIn[2*Step+i]; - for ( i = 0; i < Step; i++ ) - pOut[2*Step+i] = pIn[Step+i]; - for ( i = 0; i < Step; i++ ) - pOut[3*Step+i] = pIn[3*Step+i]; - pIn += 4*Step; - pOut += 4*Step; - } - } - else // if ( iVar == 4 ) - { - for ( i = 0; i < nWords; i += 2 ) - { - pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16); - pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16); - } - } -} - -/**Function************************************************************* - - Synopsis [Swaps two adjacent variables in the truth table.] - - Description [Swaps var number Start and var number Start+1 (0-based numbers). - The input truth table is pIn. The output truth table is pOut.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_TruthSwapAdjacentVars2( unsigned * pIn, unsigned * pOut, int nVars, int Start ) -{ - int nWords = (nVars <= 5)? 1 : (1 << (nVars-5)); - int i, k, Step; - - assert( Start < nVars - 1 ); - switch ( Start ) - { - case 0: - for ( i = 0; i < nWords; i++ ) - pOut[i] = (pIn[i] & 0x99999999) | ((pIn[i] & 0x22222222) << 1) | ((pIn[i] & 0x44444444) >> 1); - return; - case 1: - for ( i = 0; i < nWords; i++ ) - pOut[i] = (pIn[i] & 0xC3C3C3C3) | ((pIn[i] & 0x0C0C0C0C) << 2) | ((pIn[i] & 0x30303030) >> 2); - return; - case 2: - for ( i = 0; i < nWords; i++ ) - pOut[i] = (pIn[i] & 0xF00FF00F) | ((pIn[i] & 0x00F000F0) << 4) | ((pIn[i] & 0x0F000F00) >> 4); - return; - case 3: - for ( i = 0; i < nWords; i++ ) - pOut[i] = (pIn[i] & 0xFF0000FF) | ((pIn[i] & 0x0000FF00) << 8) | ((pIn[i] & 0x00FF0000) >> 8); - return; - case 4: - for ( i = 0; i < nWords; i += 2 ) - { - pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16); - pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16); - } - return; - default: - Step = (1 << (Start - 5)); - for ( k = 0; k < nWords; k += 4*Step ) - { - for ( i = 0; i < Step; i++ ) - pOut[i] = pIn[i]; - for ( i = 0; i < Step; i++ ) - pOut[Step+i] = pIn[2*Step+i]; - for ( i = 0; i < Step; i++ ) - pOut[2*Step+i] = pIn[Step+i]; - for ( i = 0; i < Step; i++ ) - pOut[3*Step+i] = pIn[3*Step+i]; - pIn += 4*Step; - pOut += 4*Step; - } - return; - } -} - -/**Function************************************************************* - - Synopsis [Expands the truth table according to the phase.] - - Description [The input and output truth tables are in pIn/pOut. The current number - of variables is nVars. The total number of variables in nVarsAll. The last argument - (Phase) contains shows where the variables should go.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase ) -{ - unsigned * pTemp; - int i, k, Var = nVars - 1, Counter = 0; - for ( i = nVarsAll - 1; i >= 0; i-- ) - if ( Phase & (1 << i) ) - { - for ( k = Var; k < i; k++ ) - { - Extra_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k ); - pTemp = pIn; pIn = pOut; pOut = pTemp; - Counter++; - } - Var--; - } - assert( Var == -1 ); - // swap if it was moved an even number of times - if ( !(Counter & 1) ) - Extra_TruthCopy( pOut, pIn, nVarsAll ); -} - -/**Function************************************************************* - - Synopsis [Shrinks the truth table according to the phase.] - - Description [The input and output truth tables are in pIn/pOut. The current number - of variables is nVars. The total number of variables in nVarsAll. The last argument - (Phase) contains shows what variables should remain.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase ) -{ - unsigned * pTemp; - int i, k, Var = 0, Counter = 0; - for ( i = 0; i < nVarsAll; i++ ) - if ( Phase & (1 << i) ) - { - for ( k = i-1; k >= Var; k-- ) - { - Extra_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k ); - pTemp = pIn; pIn = pOut; pOut = pTemp; - Counter++; - } - Var++; - } - assert( Var == nVars ); - // swap if it was moved an even number of times - if ( !(Counter & 1) ) - Extra_TruthCopy( pOut, pIn, nVarsAll ); -} - - -/**Function************************************************************* - - Synopsis [Returns 1 if TT depends on the given variable.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Extra_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar ) -{ - int nWords = Extra_TruthWordNum( nVars ); - int i, k, Step; - - assert( iVar < nVars ); - switch ( iVar ) - { - case 0: - for ( i = 0; i < nWords; i++ ) - if ( (pTruth[i] & 0x55555555) != ((pTruth[i] & 0xAAAAAAAA) >> 1) ) - return 1; - return 0; - case 1: - for ( i = 0; i < nWords; i++ ) - if ( (pTruth[i] & 0x33333333) != ((pTruth[i] & 0xCCCCCCCC) >> 2) ) - return 1; - return 0; - case 2: - for ( i = 0; i < nWords; i++ ) - if ( (pTruth[i] & 0x0F0F0F0F) != ((pTruth[i] & 0xF0F0F0F0) >> 4) ) - return 1; - return 0; - case 3: - for ( i = 0; i < nWords; i++ ) - if ( (pTruth[i] & 0x00FF00FF) != ((pTruth[i] & 0xFF00FF00) >> 8) ) - return 1; - return 0; - case 4: - for ( i = 0; i < nWords; i++ ) - if ( (pTruth[i] & 0x0000FFFF) != ((pTruth[i] & 0xFFFF0000) >> 16) ) - return 1; - return 0; - default: - Step = (1 << (iVar - 5)); - for ( k = 0; k < nWords; k += 2*Step ) - { - for ( i = 0; i < Step; i++ ) - if ( pTruth[i] != pTruth[Step+i] ) - return 1; - pTruth += 2*Step; - } - return 0; - } -} - -/**Function************************************************************* - - Synopsis [Returns the number of support vars.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Extra_TruthSupportSize( unsigned * pTruth, int nVars ) -{ - int i, Counter = 0; - for ( i = 0; i < nVars; i++ ) - Counter += Extra_TruthVarInSupport( pTruth, nVars, i ); - return Counter; -} - -/**Function************************************************************* - - Synopsis [Returns support of the function.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Extra_TruthSupport( unsigned * pTruth, int nVars ) -{ - int i, Support = 0; - for ( i = 0; i < nVars; i++ ) - if ( Extra_TruthVarInSupport( pTruth, nVars, i ) ) - Support |= (1 << i); - return Support; -} - - - -/**Function************************************************************* - - Synopsis [Computes positive cofactor of the function.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_TruthCofactor1( unsigned * pTruth, int nVars, int iVar ) -{ - int nWords = Extra_TruthWordNum( nVars ); - int i, k, Step; - - assert( iVar < nVars ); - switch ( iVar ) - { - case 0: - for ( i = 0; i < nWords; i++ ) - pTruth[i] = (pTruth[i] & 0xAAAAAAAA) | ((pTruth[i] & 0xAAAAAAAA) >> 1); - return; - case 1: - for ( i = 0; i < nWords; i++ ) - pTruth[i] = (pTruth[i] & 0xCCCCCCCC) | ((pTruth[i] & 0xCCCCCCCC) >> 2); - return; - case 2: - for ( i = 0; i < nWords; i++ ) - pTruth[i] = (pTruth[i] & 0xF0F0F0F0) | ((pTruth[i] & 0xF0F0F0F0) >> 4); - return; - case 3: - for ( i = 0; i < nWords; i++ ) - pTruth[i] = (pTruth[i] & 0xFF00FF00) | ((pTruth[i] & 0xFF00FF00) >> 8); - return; - case 4: - for ( i = 0; i < nWords; i++ ) - pTruth[i] = (pTruth[i] & 0xFFFF0000) | ((pTruth[i] & 0xFFFF0000) >> 16); - return; - default: - Step = (1 << (iVar - 5)); - for ( k = 0; k < nWords; k += 2*Step ) - { - for ( i = 0; i < Step; i++ ) - pTruth[i] = pTruth[Step+i]; - pTruth += 2*Step; - } - return; - } -} - -/**Function************************************************************* - - Synopsis [Computes negative cofactor of the function.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_TruthCofactor0( unsigned * pTruth, int nVars, int iVar ) -{ - int nWords = Extra_TruthWordNum( nVars ); - int i, k, Step; - - assert( iVar < nVars ); - switch ( iVar ) - { - case 0: - for ( i = 0; i < nWords; i++ ) - pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1); - return; - case 1: - for ( i = 0; i < nWords; i++ ) - pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2); - return; - case 2: - for ( i = 0; i < nWords; i++ ) - pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4); - return; - case 3: - for ( i = 0; i < nWords; i++ ) - pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8); - return; - case 4: - for ( i = 0; i < nWords; i++ ) - pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16); - return; - default: - Step = (1 << (iVar - 5)); - for ( k = 0; k < nWords; k += 2*Step ) - { - for ( i = 0; i < Step; i++ ) - pTruth[Step+i] = pTruth[i]; - pTruth += 2*Step; - } - return; - } -} - - -/**Function************************************************************* - - Synopsis [Existentially quantifies the variable.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_TruthExist( unsigned * pTruth, int nVars, int iVar ) -{ - int nWords = Extra_TruthWordNum( nVars ); - int i, k, Step; - - assert( iVar < nVars ); - switch ( iVar ) - { - case 0: - for ( i = 0; i < nWords; i++ ) - pTruth[i] |= ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1); - return; - case 1: - for ( i = 0; i < nWords; i++ ) - pTruth[i] |= ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2); - return; - case 2: - for ( i = 0; i < nWords; i++ ) - pTruth[i] |= ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4); - return; - case 3: - for ( i = 0; i < nWords; i++ ) - pTruth[i] |= ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8); - return; - case 4: - for ( i = 0; i < nWords; i++ ) - pTruth[i] |= ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16); - return; - default: - Step = (1 << (iVar - 5)); - for ( k = 0; k < nWords; k += 2*Step ) - { - for ( i = 0; i < Step; i++ ) - { - pTruth[i] |= pTruth[Step+i]; - pTruth[Step+i] = pTruth[i]; - } - pTruth += 2*Step; - } - return; - } -} - -/**Function************************************************************* - - Synopsis [Existentially quantifies the variable.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_TruthForall( unsigned * pTruth, int nVars, int iVar ) -{ - int nWords = Extra_TruthWordNum( nVars ); - int i, k, Step; - - assert( iVar < nVars ); - switch ( iVar ) - { - case 0: - for ( i = 0; i < nWords; i++ ) - pTruth[i] &= ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1); - return; - case 1: - for ( i = 0; i < nWords; i++ ) - pTruth[i] &= ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2); - return; - case 2: - for ( i = 0; i < nWords; i++ ) - pTruth[i] &= ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4); - return; - case 3: - for ( i = 0; i < nWords; i++ ) - pTruth[i] &= ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8); - return; - case 4: - for ( i = 0; i < nWords; i++ ) - pTruth[i] &= ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16); - return; - default: - Step = (1 << (iVar - 5)); - for ( k = 0; k < nWords; k += 2*Step ) - { - for ( i = 0; i < Step; i++ ) - { - pTruth[i] &= pTruth[Step+i]; - pTruth[Step+i] = pTruth[i]; - } - pTruth += 2*Step; - } - return; - } -} - - -/**Function************************************************************* - - Synopsis [Computes negative cofactor of the function.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar ) -{ - int nWords = Extra_TruthWordNum( nVars ); - int i, k, Step; - - assert( iVar < nVars ); - switch ( iVar ) - { - case 0: - for ( i = 0; i < nWords; i++ ) - pOut[i] = (pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA); - return; - case 1: - for ( i = 0; i < nWords; i++ ) - pOut[i] = (pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC); - return; - case 2: - for ( i = 0; i < nWords; i++ ) - pOut[i] = (pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0); - return; - case 3: - for ( i = 0; i < nWords; i++ ) - pOut[i] = (pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00); - return; - case 4: - for ( i = 0; i < nWords; i++ ) - pOut[i] = (pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000); - return; - default: - Step = (1 << (iVar - 5)); - for ( k = 0; k < nWords; k += 2*Step ) - { - for ( i = 0; i < Step; i++ ) - { - pOut[i] = pCof0[i]; - pOut[Step+i] = pCof1[Step+i]; - } - pOut += 2*Step; - } - return; - } -} - -/**Function************************************************************* - - Synopsis [Checks symmetry of two variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Extra_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 ) -{ - static unsigned uTemp0[16], uTemp1[16]; - assert( nVars <= 9 ); - // compute Cof01 - Extra_TruthCopy( uTemp0, pTruth, nVars ); - Extra_TruthCofactor0( uTemp0, nVars, iVar0 ); - Extra_TruthCofactor1( uTemp0, nVars, iVar1 ); - // compute Cof10 - Extra_TruthCopy( uTemp1, pTruth, nVars ); - Extra_TruthCofactor1( uTemp1, nVars, iVar0 ); - Extra_TruthCofactor0( uTemp1, nVars, iVar1 ); - // compare - return Extra_TruthIsEqual( uTemp0, uTemp1, nVars ); -} - -/**Function************************************************************* - - Synopsis [Checks antisymmetry of two variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Extra_TruthVarsAntiSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 ) -{ - static unsigned uTemp0[16], uTemp1[16]; - assert( nVars <= 9 ); - // compute Cof00 - Extra_TruthCopy( uTemp0, pTruth, nVars ); - Extra_TruthCofactor0( uTemp0, nVars, iVar0 ); - Extra_TruthCofactor0( uTemp0, nVars, iVar1 ); - // compute Cof11 - Extra_TruthCopy( uTemp1, pTruth, nVars ); - Extra_TruthCofactor1( uTemp1, nVars, iVar0 ); - Extra_TruthCofactor1( uTemp1, nVars, iVar1 ); - // compare - return Extra_TruthIsEqual( uTemp0, uTemp1, nVars ); -} - -/**Function************************************************************* - - Synopsis [Changes phase of the function w.r.t. one variable.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_TruthChangePhase( unsigned * pTruth, int nVars, int iVar ) -{ - int nWords = Extra_TruthWordNum( nVars ); - int i, k, Step; - unsigned Temp; - - assert( iVar < nVars ); - switch ( iVar ) - { - case 0: - for ( i = 0; i < nWords; i++ ) - pTruth[i] = ((pTruth[i] & 0x55555555) << 1) | ((pTruth[i] & 0xAAAAAAAA) >> 1); - return; - case 1: - for ( i = 0; i < nWords; i++ ) - pTruth[i] = ((pTruth[i] & 0x33333333) << 2) | ((pTruth[i] & 0xCCCCCCCC) >> 2); - return; - case 2: - for ( i = 0; i < nWords; i++ ) - pTruth[i] = ((pTruth[i] & 0x0F0F0F0F) << 4) | ((pTruth[i] & 0xF0F0F0F0) >> 4); - return; - case 3: - for ( i = 0; i < nWords; i++ ) - pTruth[i] = ((pTruth[i] & 0x00FF00FF) << 8) | ((pTruth[i] & 0xFF00FF00) >> 8); - return; - case 4: - for ( i = 0; i < nWords; i++ ) - pTruth[i] = ((pTruth[i] & 0x0000FFFF) << 16) | ((pTruth[i] & 0xFFFF0000) >> 16); - return; - default: - Step = (1 << (iVar - 5)); - for ( k = 0; k < nWords; k += 2*Step ) - { - for ( i = 0; i < Step; i++ ) - { - Temp = pTruth[i]; - pTruth[i] = pTruth[Step+i]; - pTruth[Step+i] = Temp; - } - pTruth += 2*Step; - } - return; - } -} - -/**Function************************************************************* - - Synopsis [Computes minimum overlap in supports of cofactors.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Extra_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin ) -{ - static unsigned uCofactor[16]; - int i, ValueCur, ValueMin, VarMin; - unsigned uSupp0, uSupp1; - int nVars0, nVars1; - assert( nVars <= 9 ); - ValueMin = 32; - VarMin = -1; - for ( i = 0; i < nVars; i++ ) - { - // get negative cofactor - Extra_TruthCopy( uCofactor, pTruth, nVars ); - Extra_TruthCofactor0( uCofactor, nVars, i ); - uSupp0 = Extra_TruthSupport( uCofactor, nVars ); - nVars0 = Extra_WordCountOnes( uSupp0 ); -//Extra_PrintBinary( stdout, &uSupp0, 8 ); printf( "\n" ); - // get positive cofactor - Extra_TruthCopy( uCofactor, pTruth, nVars ); - Extra_TruthCofactor1( uCofactor, nVars, i ); - uSupp1 = Extra_TruthSupport( uCofactor, nVars ); - nVars1 = Extra_WordCountOnes( uSupp1 ); -//Extra_PrintBinary( stdout, &uSupp1, 8 ); printf( "\n" ); - // get the number of common vars - ValueCur = Extra_WordCountOnes( uSupp0 & uSupp1 ); - if ( ValueMin > ValueCur && nVars0 <= 5 && nVars1 <= 5 ) - { - ValueMin = ValueCur; - VarMin = i; - } - if ( ValueMin == 0 ) - break; - } - if ( pVarMin ) - *pVarMin = VarMin; - return ValueMin; -} - - -/**Function************************************************************* - - Synopsis [Counts the number of 1's in each cofactor.] - - Description [The resulting numbers are stored in the array of shorts, - whose length is 2*nVars. The number of 1's is counted in a different - space than the original function. For example, if the function depends - on k variables, the cofactors are assumed to depend on k-1 variables.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore ) -{ - int nWords = Extra_TruthWordNum( nVars ); - int i, k, Counter; - memset( pStore, 0, sizeof(short) * 2 * nVars ); - if ( nVars <= 5 ) - { - if ( nVars > 0 ) - { - pStore[2*0+0] = Extra_WordCountOnes( pTruth[0] & 0x55555555 ); - pStore[2*0+1] = Extra_WordCountOnes( pTruth[0] & 0xAAAAAAAA ); - } - if ( nVars > 1 ) - { - pStore[2*1+0] = Extra_WordCountOnes( pTruth[0] & 0x33333333 ); - pStore[2*1+1] = Extra_WordCountOnes( pTruth[0] & 0xCCCCCCCC ); - } - if ( nVars > 2 ) - { - pStore[2*2+0] = Extra_WordCountOnes( pTruth[0] & 0x0F0F0F0F ); - pStore[2*2+1] = Extra_WordCountOnes( pTruth[0] & 0xF0F0F0F0 ); - } - if ( nVars > 3 ) - { - pStore[2*3+0] = Extra_WordCountOnes( pTruth[0] & 0x00FF00FF ); - pStore[2*3+1] = Extra_WordCountOnes( pTruth[0] & 0xFF00FF00 ); - } - if ( nVars > 4 ) - { - pStore[2*4+0] = Extra_WordCountOnes( pTruth[0] & 0x0000FFFF ); - pStore[2*4+1] = Extra_WordCountOnes( pTruth[0] & 0xFFFF0000 ); - } - return; - } - // nVars >= 6 - // count 1's for all other variables - for ( k = 0; k < nWords; k++ ) - { - Counter = Extra_WordCountOnes( pTruth[k] ); - for ( i = 5; i < nVars; i++ ) - if ( k & (1 << (i-5)) ) - pStore[2*i+1] += Counter; - else - pStore[2*i+0] += Counter; - } - // count 1's for the first five variables - for ( k = 0; k < nWords/2; k++ ) - { - pStore[2*0+0] += Extra_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) << 1) ); - pStore[2*0+1] += Extra_WordCountOnes( (pTruth[0] & 0xAAAAAAAA) | ((pTruth[1] & 0xAAAAAAAA) >> 1) ); - pStore[2*1+0] += Extra_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) << 2) ); - pStore[2*1+1] += Extra_WordCountOnes( (pTruth[0] & 0xCCCCCCCC) | ((pTruth[1] & 0xCCCCCCCC) >> 2) ); - pStore[2*2+0] += Extra_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) << 4) ); - pStore[2*2+1] += Extra_WordCountOnes( (pTruth[0] & 0xF0F0F0F0) | ((pTruth[1] & 0xF0F0F0F0) >> 4) ); - pStore[2*3+0] += Extra_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) << 8) ); - pStore[2*3+1] += Extra_WordCountOnes( (pTruth[0] & 0xFF00FF00) | ((pTruth[1] & 0xFF00FF00) >> 8) ); - pStore[2*4+0] += Extra_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) ); - pStore[2*4+1] += Extra_WordCountOnes( (pTruth[0] & 0xFFFF0000) | ((pTruth[1] & 0xFFFF0000) >> 16) ); - pTruth += 2; - } -} - - -/**Function************************************************************* - - Synopsis [Canonicize the truth table.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned Extra_TruthHash( unsigned * pIn, int nWords ) -{ - // The 1,024 smallest prime numbers used to compute the hash value - // http://www.math.utah.edu/~alfeld/math/primelist.html - static int HashPrimes[1024] = { 2, 3, 5, - 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97, - 101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151, 157, 163, 167, 173, 179, 181, 191, - 193, 197, 199, 211, 223, 227, 229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281, 283, - 293, 307, 311, 313, 317, 331, 337, 347, 349, 353, 359, 367, 373, 379, 383, 389, 397, 401, - 409, 419, 421, 431, 433, 439, 443, 449, 457, 461, 463, 467, 479, 487, 491, 499, 503, 509, - 521, 523, 541, 547, 557, 563, 569, 571, 577, 587, 593, 599, 601, 607, 613, 617, 619, 631, - 641, 643, 647, 653, 659, 661, 673, 677, 683, 691, 701, 709, 719, 727, 733, 739, 743, 751, - 757, 761, 769, 773, 787, 797, 809, 811, 821, 823, 827, 829, 839, 853, 857, 859, 863, 877, - 881, 883, 887, 907, 911, 919, 929, 937, 941, 947, 953, 967, 971, 977, 983, 991, 997, - 1009, 1013, 1019, 1021, 1031, 1033, 1039, 1049, 1051, 1061, 1063, 1069, 1087, 1091, - 1093, 1097, 1103, 1109, 1117, 1123, 1129, 1151, 1153, 1163, 1171, 1181, 1187, 1193, - 1201, 1213, 1217, 1223, 1229, 1231, 1237, 1249, 1259, 1277, 1279, 1283, 1289, 1291, - 1297, 1301, 1303, 1307, 1319, 1321, 1327, 1361, 1367, 1373, 1381, 1399, 1409, 1423, - 1427, 1429, 1433, 1439, 1447, 1451, 1453, 1459, 1471, 1481, 1483, 1487, 1489, 1493, - 1499, 1511, 1523, 1531, 1543, 1549, 1553, 1559, 1567, 1571, 1579, 1583, 1597, 1601, - 1607, 1609, 1613, 1619, 1621, 1627, 1637, 1657, 1663, 1667, 1669, 1693, 1697, 1699, - 1709, 1721, 1723, 1733, 1741, 1747, 1753, 1759, 1777, 1783, 1787, 1789, 1801, 1811, - 1823, 1831, 1847, 1861, 1867, 1871, 1873, 1877, 1879, 1889, 1901, 1907, 1913, 1931, - 1933, 1949, 1951, 1973, 1979, 1987, 1993, 1997, 1999, 2003, 2011, 2017, 2027, 2029, - 2039, 2053, 2063, 2069, 2081, 2083, 2087, 2089, 2099, 2111, 2113, 2129, 2131, 2137, - 2141, 2143, 2153, 2161, 2179, 2203, 2207, 2213, 2221, 2237, 2239, 2243, 2251, 2267, - 2269, 2273, 2281, 2287, 2293, 2297, 2309, 2311, 2333, 2339, 2341, 2347, 2351, 2357, - 2371, 2377, 2381, 2383, 2389, 2393, 2399, 2411, 2417, 2423, 2437, 2441, 2447, 2459, - 2467, 2473, 2477, 2503, 2521, 2531, 2539, 2543, 2549, 2551, 2557, 2579, 2591, 2593, - 2609, 2617, 2621, 2633, 2647, 2657, 2659, 2663, 2671, 2677, 2683, 2687, 2689, 2693, - 2699, 2707, 2711, 2713, 2719, 2729, 2731, 2741, 2749, 2753, 2767, 2777, 2789, 2791, - 2797, 2801, 2803, 2819, 2833, 2837, 2843, 2851, 2857, 2861, 2879, 2887, 2897, 2903, - 2909, 2917, 2927, 2939, 2953, 2957, 2963, 2969, 2971, 2999, 3001, 3011, 3019, 3023, - 3037, 3041, 3049, 3061, 3067, 3079, 3083, 3089, 3109, 3119, 3121, 3137, 3163, 3167, - 3169, 3181, 3187, 3191, 3203, 3209, 3217, 3221, 3229, 3251, 3253, 3257, 3259, 3271, - 3299, 3301, 3307, 3313, 3319, 3323, 3329, 3331, 3343, 3347, 3359, 3361, 3371, 3373, - 3389, 3391, 3407, 3413, 3433, 3449, 3457, 3461, 3463, 3467, 3469, 3491, 3499, 3511, - 3517, 3527, 3529, 3533, 3539, 3541, 3547, 3557, 3559, 3571, 3581, 3583, 3593, 3607, - 3613, 3617, 3623, 3631, 3637, 3643, 3659, 3671, 3673, 3677, 3691, 3697, 3701, 3709, - 3719, 3727, 3733, 3739, 3761, 3767, 3769, 3779, 3793, 3797, 3803, 3821, 3823, 3833, - 3847, 3851, 3853, 3863, 3877, 3881, 3889, 3907, 3911, 3917, 3919, 3923, 3929, 3931, - 3943, 3947, 3967, 3989, 4001, 4003, 4007, 4013, 4019, 4021, 4027, 4049, 4051, 4057, - 4073, 4079, 4091, 4093, 4099, 4111, 4127, 4129, 4133, 4139, 4153, 4157, 4159, 4177, - 4201, 4211, 4217, 4219, 4229, 4231, 4241, 4243, 4253, 4259, 4261, 4271, 4273, 4283, - 4289, 4297, 4327, 4337, 4339, 4349, 4357, 4363, 4373, 4391, 4397, 4409, 4421, 4423, - 4441, 4447, 4451, 4457, 4463, 4481, 4483, 4493, 4507, 4513, 4517, 4519, 4523, 4547, - 4549, 4561, 4567, 4583, 4591, 4597, 4603, 4621, 4637, 4639, 4643, 4649, 4651, 4657, - 4663, 4673, 4679, 4691, 4703, 4721, 4723, 4729, 4733, 4751, 4759, 4783, 4787, 4789, - 4793, 4799, 4801, 4813, 4817, 4831, 4861, 4871, 4877, 4889, 4903, 4909, 4919, 4931, - 4933, 4937, 4943, 4951, 4957, 4967, 4969, 4973, 4987, 4993, 4999, 5003, 5009, 5011, - 5021, 5023, 5039, 5051, 5059, 5077, 5081, 5087, 5099, 5101, 5107, 5113, 5119, 5147, - 5153, 5167, 5171, 5179, 5189, 5197, 5209, 5227, 5231, 5233, 5237, 5261, 5273, 5279, - 5281, 5297, 5303, 5309, 5323, 5333, 5347, 5351, 5381, 5387, 5393, 5399, 5407, 5413, - 5417, 5419, 5431, 5437, 5441, 5443, 5449, 5471, 5477, 5479, 5483, 5501, 5503, 5507, - 5519, 5521, 5527, 5531, 5557, 5563, 5569, 5573, 5581, 5591, 5623, 5639, 5641, 5647, - 5651, 5653, 5657, 5659, 5669, 5683, 5689, 5693, 5701, 5711, 5717, 5737, 5741, 5743, - 5749, 5779, 5783, 5791, 5801, 5807, 5813, 5821, 5827, 5839, 5843, 5849, 5851, 5857, - 5861, 5867, 5869, 5879, 5881, 5897, 5903, 5923, 5927, 5939, 5953, 5981, 5987, 6007, - 6011, 6029, 6037, 6043, 6047, 6053, 6067, 6073, 6079, 6089, 6091, 6101, 6113, 6121, - 6131, 6133, 6143, 6151, 6163, 6173, 6197, 6199, 6203, 6211, 6217, 6221, 6229, 6247, - 6257, 6263, 6269, 6271, 6277, 6287, 6299, 6301, 6311, 6317, 6323, 6329, 6337, 6343, - 6353, 6359, 6361, 6367, 6373, 6379, 6389, 6397, 6421, 6427, 6449, 6451, 6469, 6473, - 6481, 6491, 6521, 6529, 6547, 6551, 6553, 6563, 6569, 6571, 6577, 6581, 6599, 6607, - 6619, 6637, 6653, 6659, 6661, 6673, 6679, 6689, 6691, 6701, 6703, 6709, 6719, 6733, - 6737, 6761, 6763, 6779, 6781, 6791, 6793, 6803, 6823, 6827, 6829, 6833, 6841, 6857, - 6863, 6869, 6871, 6883, 6899, 6907, 6911, 6917, 6947, 6949, 6959, 6961, 6967, 6971, - 6977, 6983, 6991, 6997, 7001, 7013, 7019, 7027, 7039, 7043, 7057, 7069, 7079, 7103, - 7109, 7121, 7127, 7129, 7151, 7159, 7177, 7187, 7193, 7207, 7211, 7213, 7219, 7229, - 7237, 7243, 7247, 7253, 7283, 7297, 7307, 7309, 7321, 7331, 7333, 7349, 7351, 7369, - 7393, 7411, 7417, 7433, 7451, 7457, 7459, 7477, 7481, 7487, 7489, 7499, 7507, 7517, - 7523, 7529, 7537, 7541, 7547, 7549, 7559, 7561, 7573, 7577, 7583, 7589, 7591, 7603, - 7607, 7621, 7639, 7643, 7649, 7669, 7673, 7681, 7687, 7691, 7699, 7703, 7717, 7723, - 7727, 7741, 7753, 7757, 7759, 7789, 7793, 7817, 7823, 7829, 7841, 7853, 7867, 7873, - 7877, 7879, 7883, 7901, 7907, 7919, 7927, 7933, 7937, 7949, 7951, 7963, 7993, 8009, - 8011, 8017, 8039, 8053, 8059, 8069, 8081, 8087, 8089, 8093, 8101, 8111, 8117, 8123, - 8147, 8161 }; - int i; - unsigned uHashKey; - assert( nWords <= 1024 ); - uHashKey = 0; - for ( i = 0; i < nWords; i++ ) - uHashKey ^= HashPrimes[i] * pIn[i]; - return uHashKey; -} - - -/**Function************************************************************* - - Synopsis [Canonicize the truth table.] - - Description [Returns the phase. ] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned Extra_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore ) -{ - unsigned * pIn = pInOut, * pOut = pAux, * pTemp; - int nWords = Extra_TruthWordNum( nVars ); - int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit; - unsigned uCanonPhase; - - // canonicize output - uCanonPhase = 0; - nOnes = Extra_TruthCountOnes(pIn, nVars); - if ( (nOnes > nWords * 16) || ((nOnes == nWords * 16) && (pIn[0] & 1)) ) - { - uCanonPhase |= (1 << nVars); - Extra_TruthNot( pIn, pIn, nVars ); - } - - // collect the minterm counts - Extra_TruthCountOnesInCofs( pIn, nVars, pStore ); - - // canonicize phase - for ( i = 0; i < nVars; i++ ) - { - if ( pStore[2*i+0] <= pStore[2*i+1] ) - continue; - uCanonPhase |= (1 << i); - Temp = pStore[2*i+0]; - pStore[2*i+0] = pStore[2*i+1]; - pStore[2*i+1] = Temp; - Extra_TruthChangePhase( pIn, nVars, i ); - } - -// Extra_PrintHexadecimal( stdout, pIn, nVars ); -// printf( "\n" ); - - // permute - Counter = 0; - do { - fChange = 0; - for ( i = 0; i < nVars-1; i++ ) - { - if ( pStore[2*i] <= pStore[2*(i+1)] ) - continue; - Counter++; - fChange = 1; - - Temp = pCanonPerm[i]; - pCanonPerm[i] = pCanonPerm[i+1]; - pCanonPerm[i+1] = Temp; - - Temp = pStore[2*i]; - pStore[2*i] = pStore[2*(i+1)]; - pStore[2*(i+1)] = Temp; - - Temp = pStore[2*i+1]; - pStore[2*i+1] = pStore[2*(i+1)+1]; - pStore[2*(i+1)+1] = Temp; - - Extra_TruthSwapAdjacentVars( pOut, pIn, nVars, i ); - pTemp = pIn; pIn = pOut; pOut = pTemp; - } - } while ( fChange ); - -/* - Extra_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " ); - for ( i = 0; i < nVars; i++ ) - printf( "%d=%d/%d ", pCanonPerm[i], pStore[2*i], pStore[2*i+1] ); - printf( " C = %d\n", Counter ); - Extra_PrintHexadecimal( stdout, pIn, nVars ); - printf( "\n" ); -*/ - -/* - // process symmetric variable groups - uSymms = 0; - for ( i = 0; i < nVars-1; i++ ) - { - if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric - continue; - if ( pStore[2*i] != pStore[2*i+1] ) - continue; - if ( Extra_TruthVarsSymm( pIn, nVars, i, i+1 ) ) - continue; - if ( Extra_TruthVarsAntiSymm( pIn, nVars, i, i+1 ) ) - Extra_TruthChangePhase( pIn, nVars, i+1 ); - } -*/ - -/* - // process symmetric variable groups - uSymms = 0; - for ( i = 0; i < nVars-1; i++ ) - { - if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric - continue; - // i and i+1 can be symmetric - // find the end of this group - for ( k = i+1; k < nVars; k++ ) - if ( pStore[2*i] != pStore[2*k] ) - break; - Limit = k; - assert( i < Limit-1 ); - // go through the variables in this group - for ( j = i + 1; j < Limit; j++ ) - { - // check symmetry - if ( Extra_TruthVarsSymm( pIn, nVars, i, j ) ) - { - uSymms |= (1 << j); - continue; - } - // they are phase-unknown - if ( pStore[2*i] == pStore[2*i+1] ) - { - if ( Extra_TruthVarsAntiSymm( pIn, nVars, i, j ) ) - { - Extra_TruthChangePhase( pIn, nVars, j ); - uCanonPhase ^= (1 << j); - uSymms |= (1 << j); - continue; - } - } - - // they are not symmetric - move j as far as it goes in the group - for ( k = j; k < Limit-1; k++ ) - { - Counter++; - - Temp = pCanonPerm[k]; - pCanonPerm[k] = pCanonPerm[k+1]; - pCanonPerm[k+1] = Temp; - - assert( pStore[2*k] == pStore[2*(k+1)] ); - Extra_TruthSwapAdjacentVars( pOut, pIn, nVars, k ); - pTemp = pIn; pIn = pOut; pOut = pTemp; - } - Limit--; - j--; - } - i = Limit - 1; - } -*/ - - // swap if it was moved an even number of times - if ( Counter & 1 ) - Extra_TruthCopy( pOut, pIn, nVars ); - return uCanonPhase; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/misc/extra/extraUtilUtil.c b/src/misc/extra/extraUtilUtil.c deleted file mode 100644 index c685f7bc..00000000 --- a/src/misc/extra/extraUtilUtil.c +++ /dev/null @@ -1,356 +0,0 @@ -/**CFile**************************************************************** - - FileName [extraUtilUtil.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [extra] - - Synopsis [Old SIS utilities.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: extraUtilUtil.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include <stdio.h> -#include "extra.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -#define EXTRA_RLIMIT_DATA_DEFAULT 67108864 // assume 64MB by default - -/* File : getopt.c - * Author : Henry Spencer, University of Toronto - * Updated: 28 April 1984 - * - * Changes: (R Rudell) - * changed index() to strchr(); - * added getopt_reset() to reset the getopt argument parsing - * - * Purpose: get option letter from argv. - */ - -char * globalUtilOptarg; // Global argument pointer (util_optarg) -int globalUtilOptind = 0; // Global argv index (util_optind) - -static char *pScanStr; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [util_cpu_time()] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -long Extra_CpuTime() -{ - return clock(); -} - -/**Function************************************************************* - - Synopsis [getSoftDataLimit()] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Extra_GetSoftDataLimit() -{ - return EXTRA_RLIMIT_DATA_DEFAULT; -} - -/**Function************************************************************* - - Synopsis [util_getopt_reset()] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_UtilGetoptReset() -{ - globalUtilOptarg = 0; - globalUtilOptind = 0; - pScanStr = 0; -} - -/**Function************************************************************* - - Synopsis [util_getopt()] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Extra_UtilGetopt( int argc, char *argv[], char *optstring ) -{ - register int c; - register char *place; - - globalUtilOptarg = NULL; - - if (pScanStr == NULL || *pScanStr == '\0') { - if (globalUtilOptind == 0) globalUtilOptind++; - if (globalUtilOptind >= argc) return EOF; - place = argv[globalUtilOptind]; - if (place[0] != '-' || place[1] == '\0') return EOF; - globalUtilOptind++; - if (place[1] == '-' && place[2] == '\0') return EOF; - pScanStr = place+1; - } - - c = *pScanStr++; - place = strchr(optstring, c); - if (place == NULL || c == ':') { - (void) fprintf(stderr, "%s: unknown option %c\n", argv[0], c); - return '?'; - } - if (*++place == ':') { - if (*pScanStr != '\0') { - globalUtilOptarg = pScanStr; - pScanStr = NULL; - } else { - if (globalUtilOptind >= argc) { - (void) fprintf(stderr, "%s: %c requires an argument\n", - argv[0], c); - return '?'; - } - globalUtilOptarg = argv[globalUtilOptind]; - globalUtilOptind++; - } - } - return c; -} - -/**Function************************************************************* - - Synopsis [util_print_time()] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Extra_UtilPrintTime( long t ) -{ - static char s[40]; - - (void) sprintf(s, "%ld.%02ld sec", t/1000, (t%1000)/10); - return s; -} - - -/**Function************************************************************* - - Synopsis [Extra_UtilStrsav()] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Extra_UtilStrsav( char *s ) -{ - if(s == NULL) { /* added 7/95, for robustness */ - return s; - } - else { - return strcpy(ALLOC(char, strlen(s)+1), s); - } -} - -/**Function************************************************************* - - Synopsis [util_tilde_expand()] - - Description [The code contributed by Niklas Sorensson.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Extra_UtilTildeExpand( char *fname ) -{ - return Extra_UtilStrsav( fname ); -/* - int n_tildes = 0; - const char* home; - char* expanded; - int length; - int i, j, k; - - for (i = 0; i < (int)strlen(fname); i++) - if (fname[i] == '~') n_tildes++; - - home = getenv("HOME"); - length = n_tildes * strlen(home) + strlen(fname); - expanded = ALLOC(char, length + 1); - - j = 0; - for (i = 0; i < (int)strlen(fname); i++){ - if (fname[i] == '~'){ - for (k = 0; k < (int)strlen(home); k++) - expanded[j++] = home[k]; - }else - expanded[j++] = fname[i]; - } - - expanded[j] = '\0'; - return expanded; -*/ -} - -/**Function************************************************************* - - Synopsis [check_file()] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Extra_UtilCheckFile(char *filename, char *mode) -{ - FILE *fp; - int got_file; - - if (strcmp(mode, "x") == 0) { - mode = "r"; - } - fp = fopen(filename, mode); - got_file = (fp != 0); - if (fp != 0) { - (void) fclose(fp); - } - return got_file; -} - -/**Function************************************************************* - - Synopsis [util_file_search()] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Extra_UtilFileSearch(char *file, char *path, char *mode) -//char *file; // file we're looking for -//char *path; // search path, colon separated -//char *mode; // "r", "w", or "x" -{ - int quit; - char *buffer, *filename, *save_path, *cp; - - if (path == 0 || strcmp(path, "") == 0) { - path = "."; /* just look in the current directory */ - } - - save_path = path = Extra_UtilStrsav(path); - quit = 0; - do { - cp = strchr(path, ':'); - if (cp != 0) { - *cp = '\0'; - } else { - quit = 1; - } - - /* cons up the filename out of the path and file name */ - if (strcmp(path, ".") == 0) { - buffer = Extra_UtilStrsav(file); - } else { - buffer = ALLOC(char, strlen(path) + strlen(file) + 4); - (void) sprintf(buffer, "%s/%s", path, file); - } - filename = Extra_UtilTildeExpand(buffer); - FREE(buffer); - - /* see if we can access it */ - if (Extra_UtilCheckFile(filename, mode)) { - FREE(save_path); - return filename; - } - FREE(filename); - path = ++cp; - } while (! quit); - - FREE(save_path); - return 0; -} - -/**Function************************************************************* - - Synopsis [MMout_of_memory()] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -/* MMout_of_memory -- out of memory for lazy people, flush and exit */ -void Extra_UtilMMout_Of_Memory( long size ) -{ - (void) fflush(stdout); - (void) fprintf(stderr, "\nout of memory allocating %u bytes\n", - (unsigned) size); - assert( 0 ); - exit(1); -} - -/**Function************************************************************* - - Synopsis [MMoutOfMemory()] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void (*Extra_UtilMMoutOfMemory)() = Extra_UtilMMout_Of_Memory; - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make index ec8bca4d..6cbf5d2c 100644 --- a/src/misc/extra/module.make +++ b/src/misc/extra/module.make @@ -1,15 +1,9 @@ -SRC += src/misc/extra/extraBddAuto.c \ - src/misc/extra/extraBddCas.c \ - src/misc/extra/extraBddKmap.c \ - src/misc/extra/extraBddMisc.c \ +SRC += src/misc/extra/extraBddMisc.c \ src/misc/extra/extraBddSymm.c \ - src/misc/extra/extraBddUnate.c \ src/misc/extra/extraUtilBitMatrix.c \ src/misc/extra/extraUtilCanon.c \ src/misc/extra/extraUtilFile.c \ src/misc/extra/extraUtilMemory.c \ src/misc/extra/extraUtilMisc.c \ src/misc/extra/extraUtilProgress.c \ - src/misc/extra/extraUtilReader.c \ - src/misc/extra/extraUtilTruth.c \ - src/misc/extra/extraUtilUtil.c + src/misc/extra/extraUtilReader.c |