summaryrefslogtreecommitdiffstats
path: root/src/misc
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc')
-rw-r--r--src/misc/extra/extra.h13
-rw-r--r--src/misc/extra/extraUtilFile.c29
-rw-r--r--src/misc/extra/extraUtilMisc.c408
-rw-r--r--src/misc/vec/vecInt.h38
4 files changed, 488 insertions, 0 deletions
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 5913e40e..7f4ec8d8 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -143,6 +143,7 @@ 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 void Extra_PrintHex( FILE * pFile, unsigned uTruth, int nVars );
extern void Extra_PrintSymbols( FILE * pFile, char Char, int nTimes, int fPrintNewLine );
/*=== extraUtilReader.c ========================================================*/
@@ -198,6 +199,18 @@ extern int * Extra_DeriveRadixCode( int Number, int Radix, int nDigits );
extern int Extra_Factorial( int n );
/* the permutation of the given number of elements */
extern char ** Extra_Permutations( int n );
+/* permutation and complementation of a truth table */
+unsigned Extra_TruthPermute( unsigned Truth, char * pPerms, int nVars, int fReverse );
+unsigned Extra_TruthPolarize( unsigned uTruth, int Polarity, int nVars );
+/* canonical forms of a truth table */
+extern unsigned Extra_TruthCanonN( unsigned uTruth, int nVars );
+extern unsigned Extra_TruthCanonNN( unsigned uTruth, int nVars );
+extern unsigned Extra_TruthCanonP( unsigned uTruth, int nVars );
+extern unsigned Extra_TruthCanonNP( unsigned uTruth, int nVars );
+extern unsigned Extra_TruthCanonNPN( unsigned uTruth, int nVars );
+/* canonical forms of 4-variable functions */
+extern void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms );
+/* for independence from CUDD */
extern unsigned int Cudd_PrimeCopy( unsigned int p );
/*=== extraUtilProgress.c ================================================================*/
diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c
index faf27dc8..03b31fea 100644
--- a/src/misc/extra/extraUtilFile.c
+++ b/src/misc/extra/extraUtilFile.c
@@ -318,6 +318,35 @@ void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits )
// fprintf( pFile, "\n" );
}
+/**Function*************************************************************
+
+ Synopsis [Prints the hex unsigned into a file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_PrintHex( FILE * pFile, unsigned uTruth, int nVars )
+{
+ int nMints, nDigits, Digit, k;
+
+ // write the number into the file
+ fprintf( pFile, "0x" );
+ nMints = (1 << nVars);
+ nDigits = nMints / 4;
+ for ( k = nDigits - 1; k >= 0; k-- )
+ {
+ Digit = ((uTruth >> (k * 4)) & 15);
+ if ( Digit < 10 )
+ fprintf( pFile, "%d", Digit );
+ else
+ fprintf( pFile, "%c", 'a' + Digit-10 );
+ }
+// fprintf( pFile, "\n" );
+}
/**Function*************************************************************
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index 41c76018..ccd871e4 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -329,6 +329,414 @@ void Extra_Permutations_rec( char ** pRes, int nFact, int n, char Array[] )
/**Function*************************************************************
+ Synopsis [Permutes the given vector of minterms.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_TruthPermute_int( int * pMints, int nMints, char * pPerm, int nVars, int * pMintsP )
+{
+ int m, v;
+ // clean the storage for minterms
+ memset( pMintsP, 0, sizeof(int) * nMints );
+ // go through minterms and add the variables
+ for ( m = 0; m < nMints; m++ )
+ for ( v = 0; v < nVars; v++ )
+ if ( pMints[m] & (1 << v) )
+ pMintsP[m] |= (1 << pPerm[v]);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Permutes the function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Extra_TruthPermute( unsigned Truth, char * pPerms, int nVars, int fReverse )
+{
+ unsigned Result;
+ int * pMints;
+ int * pMintsP;
+ int nMints;
+ int i, m;
+
+ assert( nVars < 6 );
+ nMints = (1 << nVars);
+ pMints = ALLOC( int, nMints );
+ pMintsP = ALLOC( int, nMints );
+ for ( i = 0; i < nMints; i++ )
+ pMints[i] = i;
+
+ Extra_TruthPermute_int( pMints, nMints, pPerms, nVars, pMintsP );
+
+ Result = 0;
+ if ( fReverse )
+ {
+ for ( m = 0; m < nMints; m++ )
+ if ( Truth & (1 << pMintsP[m]) )
+ Result |= (1 << m);
+ }
+ else
+ {
+ for ( m = 0; m < nMints; m++ )
+ if ( Truth & (1 << m) )
+ Result |= (1 << pMintsP[m]);
+ }
+
+ free( pMints );
+ free( pMintsP );
+
+ return Result;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Changes the phase of the function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Extra_TruthPolarize( unsigned uTruth, int Polarity, int nVars )
+{
+ // elementary truth tables
+ static unsigned Signs[5] = {
+ 0xAAAAAAAA, // 1010 1010 1010 1010 1010 1010 1010 1010
+ 0xCCCCCCCC, // 1010 1010 1010 1010 1010 1010 1010 1010
+ 0xF0F0F0F0, // 1111 0000 1111 0000 1111 0000 1111 0000
+ 0xFF00FF00, // 1111 1111 0000 0000 1111 1111 0000 0000
+ 0xFFFF0000 // 1111 1111 1111 1111 0000 0000 0000 0000
+ };
+ unsigned uTruthRes, uCof0, uCof1;
+ int nMints, Shift, v;
+ assert( nVars < 6 );
+ nMints = (1 << nVars);
+ uTruthRes = uTruth;
+ for ( v = 0; v < nVars; v++ )
+ if ( Polarity & (1 << v) )
+ {
+ uCof0 = uTruth & ~Signs[v];
+ uCof1 = uTruth & Signs[v];
+ Shift = (1 << v);
+ uCof0 <<= Shift;
+ uCof1 >>= Shift;
+ uTruth = uCof0 | uCof1;
+ }
+ if ( nVars < 5 )
+ uTruth &= ((~0) >> (32-nMints));
+ return uTruth;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes N-canonical form using brute-force methods.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Extra_TruthCanonN( unsigned uTruth, int nVars )
+{
+ unsigned uTruthMin, uPhase;
+ int nMints, p;
+ nMints = (1 << nVars);
+ uTruthMin = 0xFFFFFFFF;
+ for ( p = 0; p < nMints; p++ )
+ {
+ uPhase = Extra_TruthPolarize( uTruth, p, nVars );
+ if ( uTruthMin > uPhase )
+ uTruthMin = uPhase;
+ }
+ return uTruthMin;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes NN-canonical form using brute-force methods.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Extra_TruthCanonNN( unsigned uTruth, int nVars )
+{
+ unsigned uTruthMin, uTruthC, uPhase;
+ int nMints, p;
+ nMints = (1 << nVars);
+ uTruthC = (unsigned)( (~uTruth) & ((~((unsigned)0)) >> (32-nMints)) );
+ uTruthMin = 0xFFFFFFFF;
+ for ( p = 0; p < nMints; p++ )
+ {
+ uPhase = Extra_TruthPolarize( uTruth, p, nVars );
+ if ( uTruthMin > uPhase )
+ uTruthMin = uPhase;
+ uPhase = Extra_TruthPolarize( uTruthC, p, nVars );
+ if ( uTruthMin > uPhase )
+ uTruthMin = uPhase;
+ }
+ return uTruthMin;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes P-canonical form using brute-force methods.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Extra_TruthCanonP( unsigned uTruth, int nVars )
+{
+ static int nVarsOld, nPerms;
+ static char ** pPerms = NULL;
+
+ unsigned uTruthMin, uPerm;
+ int k;
+
+ if ( pPerms == NULL )
+ {
+ nPerms = Extra_Factorial( nVars );
+ pPerms = Extra_Permutations( nVars );
+ nVarsOld = nVars;
+ }
+ else if ( nVarsOld != nVars )
+ {
+ free( pPerms );
+ nPerms = Extra_Factorial( nVars );
+ pPerms = Extra_Permutations( nVars );
+ nVarsOld = nVars;
+ }
+
+ uTruthMin = 0xFFFFFFFF;
+ for ( k = 0; k < nPerms; k++ )
+ {
+ uPerm = Extra_TruthPermute( uTruth, pPerms[k], nVars, 0 );
+ if ( uTruthMin > uPerm )
+ uTruthMin = uPerm;
+ }
+ return uTruthMin;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes NP-canonical form using brute-force methods.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Extra_TruthCanonNP( unsigned uTruth, int nVars )
+{
+ static int nVarsOld, nPerms;
+ static char ** pPerms = NULL;
+
+ unsigned uTruthMin, uPhase, uPerm;
+ int nMints, k, p;
+
+ if ( pPerms == NULL )
+ {
+ nPerms = Extra_Factorial( nVars );
+ pPerms = Extra_Permutations( nVars );
+ nVarsOld = nVars;
+ }
+ else if ( nVarsOld != nVars )
+ {
+ free( pPerms );
+ nPerms = Extra_Factorial( nVars );
+ pPerms = Extra_Permutations( nVars );
+ nVarsOld = nVars;
+ }
+
+ nMints = (1 << nVars);
+ uTruthMin = 0xFFFFFFFF;
+ for ( p = 0; p < nMints; p++ )
+ {
+ uPhase = Extra_TruthPolarize( uTruth, p, nVars );
+ for ( k = 0; k < nPerms; k++ )
+ {
+ uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
+ if ( uTruthMin > uPerm )
+ uTruthMin = uPerm;
+ }
+ }
+ return uTruthMin;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes NPN-canonical form using brute-force methods.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Extra_TruthCanonNPN( unsigned uTruth, int nVars )
+{
+ static int nVarsOld, nPerms;
+ static char ** pPerms = NULL;
+
+ unsigned uTruthMin, uTruthC, uPhase, uPerm;
+ int nMints, k, p;
+
+ if ( pPerms == NULL )
+ {
+ nPerms = Extra_Factorial( nVars );
+ pPerms = Extra_Permutations( nVars );
+ nVarsOld = nVars;
+ }
+ else if ( nVarsOld != nVars )
+ {
+ free( pPerms );
+ nPerms = Extra_Factorial( nVars );
+ pPerms = Extra_Permutations( nVars );
+ nVarsOld = nVars;
+ }
+
+ nMints = (1 << nVars);
+ uTruthC = (unsigned)( (~uTruth) & ((~((unsigned)0)) >> (32-nMints)) );
+ uTruthMin = 0xFFFFFFFF;
+ for ( p = 0; p < nMints; p++ )
+ {
+ uPhase = Extra_TruthPolarize( uTruth, p, nVars );
+ for ( k = 0; k < nPerms; k++ )
+ {
+ uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
+ if ( uTruthMin > uPerm )
+ uTruthMin = uPerm;
+ }
+ uPhase = Extra_TruthPolarize( uTruthC, p, nVars );
+ for ( k = 0; k < nPerms; k++ )
+ {
+ uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
+ if ( uTruthMin > uPerm )
+ uTruthMin = uPerm;
+ }
+ }
+ return uTruthMin;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes NPN canonical forms for 4-variable functions.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms )
+{
+ unsigned short * uCanons;
+ unsigned uTruth, uPhase, uPerm;
+ char ** pPerms4, * uPhases, * uPerms;
+ int nFuncs, nClasses;
+ int p, k;
+
+ nFuncs = (1 << 16);
+ uCanons = ALLOC( unsigned short, nFuncs );
+ uPhases = ALLOC( char, nFuncs );
+ uPerms = ALLOC( char, nFuncs );
+ memset( uCanons, 0, sizeof(unsigned short) * nFuncs );
+ memset( uPhases, 0, sizeof(char) * nFuncs );
+ memset( uPerms, 0, sizeof(char) * nFuncs );
+ pPerms4 = Extra_Permutations( 4 );
+
+ nClasses = 1;
+ nFuncs = (1 << 15);
+ for ( uTruth = 1; uTruth < (unsigned)nFuncs; uTruth++ )
+ {
+ // skip already assigned
+ if ( uCanons[uTruth] )
+ continue;
+ nClasses++;
+ for ( p = 0; p < 16; p++ )
+ {
+ uPhase = Extra_TruthPolarize( uTruth, p, 4 );
+ for ( k = 0; k < 24; k++ )
+ {
+ uPerm = Extra_TruthPermute( uPhase, pPerms4[k], 4, 0 );
+ if ( uCanons[uPerm] == 0 )
+ {
+ uCanons[uPerm] = uTruth;
+ uPhases[uPerm] = p;
+ uPerms[uPerm] = k;
+
+ uPerm = ~uPerm & 0xFFFF;
+ uCanons[uPerm] = uTruth;
+ uPhases[uPerm] = p | 16;
+ uPerms[uPerm] = k;
+ }
+ else
+ assert( uCanons[uPerm] == uTruth );
+ }
+ uPhase = Extra_TruthPolarize( ~uTruth & 0xFFFF, p, 4 );
+ for ( k = 0; k < 24; k++ )
+ {
+ uPerm = Extra_TruthPermute( uPhase, pPerms4[k], 4, 0 );
+ if ( uCanons[uPerm] == 0 )
+ {
+ uCanons[uPerm] = uTruth;
+ uPhases[uPerm] = p;
+ uPerms[uPerm] = k;
+
+ uPerm = ~uPerm & 0xFFFF;
+ uCanons[uPerm] = uTruth;
+ uPhases[uPerm] = p | 16;
+ uPerms[uPerm] = k;
+ }
+ else
+ assert( uCanons[uPerm] == uTruth );
+ }
+ }
+ }
+ uPhases[(1<<16)-1] = 16;
+ assert( nClasses == 222 );
+ free( pPerms4 );
+ if ( puCanons )
+ *puCanons = uCanons;
+ else
+ free( uCanons );
+ if ( puPhases )
+ *puPhases = uPhases;
+ else
+ free( uPhases );
+ if ( puPerms )
+ *puPerms = uPerms;
+ else
+ free( uPerms );
+}
+
+/**Function*************************************************************
+
Synopsis [Returns the smallest prime larger than the number.]
Description []
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 76fce02e..effebc68 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -514,6 +514,44 @@ static inline void Vec_IntSort( Vec_Int_t * p, int fReverse )
(int (*)(const void *, const void *)) Vec_IntSortCompare1 );
}
+
+/**Function*************************************************************
+
+ Synopsis [Comparison procedure for two integers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Vec_IntSortCompareUnsigned( unsigned * pp1, unsigned * pp2 )
+{
+ if ( *pp1 < *pp2 )
+ return -1;
+ if ( *pp1 > *pp2 )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sorting the entries by their integer value.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Vec_IntSortUnsigned( Vec_Int_t * p )
+{
+ qsort( (void *)p->pArray, p->nSize, sizeof(int),
+ (int (*)(const void *, const void *)) Vec_IntSortCompareUnsigned );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 21:51:58 +0000