summaryrefslogtreecommitdiffstats
path: root/src/misc/extra
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc/extra')
-rw-r--r--src/misc/extra/extra.h12
-rw-r--r--src/misc/extra/extraUtilMisc.c418
2 files changed, 394 insertions, 36 deletions
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 7f4ec8d8..92e631ad 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -89,6 +89,10 @@
(((((((unsigned)(a) + (unsigned)(b)) * DD_P1 + (unsigned)(c)) * DD_P2 + \
(unsigned)(d)) * DD_P3 + (unsigned)(e)) * DD_P1) % TSIZE)
+#ifndef PRT
+#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
+#endif
+
/*===========================================================================*/
/* Various Utilities */
/*===========================================================================*/
@@ -209,7 +213,13 @@ 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 );
+extern void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap );
+extern void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** ppCounters, int nPhasesMax );
+/* 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();
/* for independence from CUDD */
extern unsigned int Cudd_PrimeCopy( unsigned int p );
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index ccd871e4..2767498b 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -246,15 +246,10 @@ char ** Extra_Permutations( int n )
{
char Array[50];
char ** pRes;
- char * pBuffer;
int nFact, i;
- // allocate all memory at once
- nFact = Extra_Factorial( n );
- pBuffer = ALLOC( char, nFact * sizeof(char *) + nFact * n * sizeof(char) );
- // split the chunk
- pRes = (char **)pBuffer;
- for ( i = 0; i < nFact; i++ )
- pRes[i] = pBuffer + nFact * sizeof(char *) + i * n * sizeof(char);
+ // allocate memory
+ nFact = Extra_Factorial( n );
+ pRes = (char **)Extra_ArrayAlloc( nFact, n, sizeof(char) );
// fill in the permutations
for ( i = 0; i < n; i++ )
Array[i] = i;
@@ -290,7 +285,7 @@ void Extra_Permutations_rec( char ** pRes, int nFact, int n, char Array[] )
{
char ** pNext;
int nFactNext;
- int iTemp, iCur, iLast, p;
+ int iTemp, iCur, iLast, k;
if ( n == 1 )
{
@@ -314,8 +309,8 @@ void Extra_Permutations_rec( char ** pRes, int nFact, int n, char Array[] )
pNext = pRes + (n - 1 - iCur) * nFactNext;
// set the last entry
- for ( p = 0; p < nFactNext; p++ )
- pNext[p][iLast] = Array[iLast];
+ for ( k = 0; k < nFactNext; k++ )
+ pNext[k][iLast] = Array[iLast];
// call recursively for this part
Extra_Permutations_rec( pNext, nFactNext, n - 1, Array );
@@ -453,12 +448,12 @@ unsigned Extra_TruthPolarize( unsigned uTruth, int Polarity, int nVars )
unsigned Extra_TruthCanonN( unsigned uTruth, int nVars )
{
unsigned uTruthMin, uPhase;
- int nMints, p;
+ int nMints, i;
nMints = (1 << nVars);
uTruthMin = 0xFFFFFFFF;
- for ( p = 0; p < nMints; p++ )
+ for ( i = 0; i < nMints; i++ )
{
- uPhase = Extra_TruthPolarize( uTruth, p, nVars );
+ uPhase = Extra_TruthPolarize( uTruth, i, nVars );
if ( uTruthMin > uPhase )
uTruthMin = uPhase;
}
@@ -479,16 +474,16 @@ unsigned Extra_TruthCanonN( unsigned uTruth, int nVars )
unsigned Extra_TruthCanonNN( unsigned uTruth, int nVars )
{
unsigned uTruthMin, uTruthC, uPhase;
- int nMints, p;
+ int nMints, i;
nMints = (1 << nVars);
uTruthC = (unsigned)( (~uTruth) & ((~((unsigned)0)) >> (32-nMints)) );
uTruthMin = 0xFFFFFFFF;
- for ( p = 0; p < nMints; p++ )
+ for ( i = 0; i < nMints; i++ )
{
- uPhase = Extra_TruthPolarize( uTruth, p, nVars );
+ uPhase = Extra_TruthPolarize( uTruth, i, nVars );
if ( uTruthMin > uPhase )
uTruthMin = uPhase;
- uPhase = Extra_TruthPolarize( uTruthC, p, nVars );
+ uPhase = Extra_TruthPolarize( uTruthC, i, nVars );
if ( uTruthMin > uPhase )
uTruthMin = uPhase;
}
@@ -555,7 +550,7 @@ unsigned Extra_TruthCanonNP( unsigned uTruth, int nVars )
static char ** pPerms = NULL;
unsigned uTruthMin, uPhase, uPerm;
- int nMints, k, p;
+ int nMints, k, i;
if ( pPerms == NULL )
{
@@ -573,9 +568,9 @@ unsigned Extra_TruthCanonNP( unsigned uTruth, int nVars )
nMints = (1 << nVars);
uTruthMin = 0xFFFFFFFF;
- for ( p = 0; p < nMints; p++ )
+ for ( i = 0; i < nMints; i++ )
{
- uPhase = Extra_TruthPolarize( uTruth, p, nVars );
+ uPhase = Extra_TruthPolarize( uTruth, i, nVars );
for ( k = 0; k < nPerms; k++ )
{
uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
@@ -603,7 +598,7 @@ unsigned Extra_TruthCanonNPN( unsigned uTruth, int nVars )
static char ** pPerms = NULL;
unsigned uTruthMin, uTruthC, uPhase, uPerm;
- int nMints, k, p;
+ int nMints, k, i;
if ( pPerms == NULL )
{
@@ -622,16 +617,16 @@ unsigned Extra_TruthCanonNPN( unsigned uTruth, int nVars )
nMints = (1 << nVars);
uTruthC = (unsigned)( (~uTruth) & ((~((unsigned)0)) >> (32-nMints)) );
uTruthMin = 0xFFFFFFFF;
- for ( p = 0; p < nMints; p++ )
+ for ( i = 0; i < nMints; i++ )
{
- uPhase = Extra_TruthPolarize( uTruth, p, nVars );
+ uPhase = Extra_TruthPolarize( uTruth, i, 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 );
+ uPhase = Extra_TruthPolarize( uTruthC, i, nVars );
for ( k = 0; k < nPerms; k++ )
{
uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
@@ -653,21 +648,24 @@ unsigned Extra_TruthCanonNPN( unsigned uTruth, int nVars )
SeeAlso []
***********************************************************************/
-void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms )
+void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap )
{
unsigned short * uCanons;
+ unsigned char * uMap;
unsigned uTruth, uPhase, uPerm;
char ** pPerms4, * uPhases, * uPerms;
int nFuncs, nClasses;
- int p, k;
+ int i, k;
nFuncs = (1 << 16);
uCanons = ALLOC( unsigned short, nFuncs );
uPhases = ALLOC( char, nFuncs );
uPerms = ALLOC( char, nFuncs );
+ uMap = ALLOC( unsigned char, nFuncs );
memset( uCanons, 0, sizeof(unsigned short) * nFuncs );
memset( uPhases, 0, sizeof(char) * nFuncs );
memset( uPerms, 0, sizeof(char) * nFuncs );
+ memset( uMap, 0, sizeof(unsigned char) * nFuncs );
pPerms4 = Extra_Permutations( 4 );
nClasses = 1;
@@ -676,41 +674,45 @@ void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** p
{
// skip already assigned
if ( uCanons[uTruth] )
+ {
+ assert( uTruth > uCanons[uTruth] );
+ uMap[uTruth] = uMap[uCanons[uTruth]];
continue;
- nClasses++;
- for ( p = 0; p < 16; p++ )
+ }
+ uMap[uTruth] = nClasses++;
+ for ( i = 0; i < 16; i++ )
{
- uPhase = Extra_TruthPolarize( uTruth, p, 4 );
+ uPhase = Extra_TruthPolarize( uTruth, i, 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;
+ uPhases[uPerm] = i;
uPerms[uPerm] = k;
uPerm = ~uPerm & 0xFFFF;
uCanons[uPerm] = uTruth;
- uPhases[uPerm] = p | 16;
+ uPhases[uPerm] = i | 16;
uPerms[uPerm] = k;
}
else
assert( uCanons[uPerm] == uTruth );
}
- uPhase = Extra_TruthPolarize( ~uTruth & 0xFFFF, p, 4 );
+ uPhase = Extra_TruthPolarize( ~uTruth & 0xFFFF, i, 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;
+ uPhases[uPerm] = i;
uPerms[uPerm] = k;
uPerm = ~uPerm & 0xFFFF;
uCanons[uPerm] = uTruth;
- uPhases[uPerm] = p | 16;
+ uPhases[uPerm] = i | 16;
uPerms[uPerm] = k;
}
else
@@ -733,6 +735,352 @@ void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** p
*puPerms = uPerms;
else
free( uPerms );
+ if ( puMap )
+ *puMap = uMap;
+ else
+ free( uMap );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes NPN canonical forms for 4-variable functions.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** ppCounters, int nPhasesMax )
+{
+ unsigned short * uCanons;
+ unsigned uTruth, uPhase;
+ char ** uPhases, * pCounters;
+ int nFuncs, nClasses, i;
+
+ nFuncs = (1 << 16);
+ uCanons = ALLOC( unsigned short, nFuncs );
+ memset( uCanons, 0, sizeof(unsigned short) * nFuncs );
+ pCounters = ALLOC( char, nFuncs );
+ memset( pCounters, 0, sizeof(char) * nFuncs );
+ uPhases = (char **)Extra_ArrayAlloc( nFuncs, nPhasesMax, sizeof(char) );
+ nClasses = 0;
+ for ( uTruth = 0; uTruth < (unsigned)nFuncs; uTruth++ )
+ {
+ // skip already assigned
+ if ( uCanons[uTruth] )
+ {
+ assert( uTruth > uCanons[uTruth] );
+ continue;
+ }
+ nClasses++;
+ for ( i = 0; i < 16; i++ )
+ {
+ uPhase = Extra_TruthPolarize( uTruth, i, 4 );
+ if ( uCanons[uPhase] == 0 )
+ {
+ uCanons[uPhase] = uTruth;
+ uPhases[uPhase][0] = i;
+ pCounters[uPhase] = 1;
+ }
+ else
+ {
+ assert( uCanons[uPhase] == uTruth );
+ if ( pCounters[uPhase] < nPhasesMax )
+ uPhases[uPhase][ pCounters[uPhase]++ ] = i;
+ }
+ }
+ }
+ if ( puCanons )
+ *puCanons = uCanons;
+ else
+ free( uCanons );
+ if ( puPhases )
+ *puPhases = uPhases;
+ else
+ free( uPhases );
+ if ( ppCounters )
+ *ppCounters = pCounters;
+ else
+ free( pCounters );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Allocated one-memory-chunk array.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void ** Extra_ArrayAlloc( int nCols, int nRows, int Size )
+{
+ char ** pRes;
+ char * pBuffer;
+ int i;
+ assert( nCols > 0 && nRows > 0 && Size > 0 );
+ pBuffer = ALLOC( char, nCols * (sizeof(void *) + nRows * Size) );
+ pRes = (char **)pBuffer;
+ pRes[0] = pBuffer + nCols * sizeof(void *);
+ for ( i = 1; i < nCols; i++ )
+ pRes[i] = pRes[0] + i * nRows * Size;
+ return pRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes a phase of the 3-var function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned short Extra_TruthPerm4One( unsigned uTruth, int Phase )
+{
+ // cases
+ static unsigned short Cases[16] = {
+ 0, // 0000 - skip
+ 0, // 0001 - skip
+ 0xCCCC, // 0010 - single var
+ 0, // 0011 - skip
+ 0xF0F0, // 0100 - single var
+ 1, // 0101
+ 1, // 0110
+ 0, // 0111 - skip
+ 0xFF00, // 1000 - single var
+ 1, // 1001
+ 1, // 1010
+ 1, // 1011
+ 1, // 1100
+ 1, // 1101
+ 1, // 1110
+ 0 // 1111 - skip
+ };
+ // permutations
+ static int Perms[16][4] = {
+ { 0, 0, 0, 0 }, // 0000 - skip
+ { 0, 0, 0, 0 }, // 0001 - skip
+ { 0, 0, 0, 0 }, // 0010 - single var
+ { 0, 0, 0, 0 }, // 0011 - skip
+ { 0, 0, 0, 0 }, // 0100 - single var
+ { 0, 2, 1, 3 }, // 0101
+ { 2, 0, 1, 3 }, // 0110
+ { 0, 0, 0, 0 }, // 0111 - skip
+ { 0, 0, 0, 0 }, // 1000 - single var
+ { 0, 2, 3, 1 }, // 1001
+ { 2, 0, 3, 1 }, // 1010
+ { 0, 1, 3, 2 }, // 1011
+ { 2, 3, 0, 1 }, // 1100
+ { 0, 3, 1, 2 }, // 1101
+ { 3, 0, 1, 2 }, // 1110
+ { 0, 0, 0, 0 } // 1111 - skip
+ };
+ int i, k, iRes;
+ unsigned uTruthRes;
+ assert( Phase >= 0 && Phase < 16 );
+ if ( Cases[Phase] == 0 )
+ return uTruth;
+ if ( Cases[Phase] > 1 )
+ return Cases[Phase];
+ uTruthRes = 0;
+ for ( i = 0; i < 16; i++ )
+ if ( uTruth & (1 << i) )
+ {
+ for ( iRes = 0, k = 0; k < 4; k++ )
+ if ( i & (1 << Perms[Phase][k]) )
+ iRes |= (1 << k);
+ uTruthRes |= (1 << iRes);
+ }
+ return uTruthRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes a phase of the 3-var function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Extra_TruthPerm5One( unsigned uTruth, int Phase )
+{
+ // cases
+ static unsigned Cases[32] = {
+ 0, // 00000 - skip
+ 0, // 00001 - skip
+ 0xCCCCCCCC, // 00010 - single var
+ 0, // 00011 - skip
+ 0xF0F0F0F0, // 00100 - single var
+ 1, // 00101
+ 1, // 00110
+ 0, // 00111 - skip
+ 0xFF00FF00, // 01000 - single var
+ 1, // 01001
+ 1, // 01010
+ 1, // 01011
+ 1, // 01100
+ 1, // 01101
+ 1, // 01110
+ 0, // 01111 - skip
+ 0xFFFF0000, // 10000 - skip
+ 1, // 10001
+ 1, // 10010
+ 1, // 10011
+ 1, // 10100
+ 1, // 10101
+ 1, // 10110
+ 1, // 10111 - four var
+ 1, // 11000
+ 1, // 11001
+ 1, // 11010
+ 1, // 11011 - four var
+ 1, // 11100
+ 1, // 11101 - four var
+ 1, // 11110 - four var
+ 0 // 11111 - skip
+ };
+ // permutations
+ static int Perms[32][5] = {
+ { 0, 0, 0, 0, 0 }, // 00000 - skip
+ { 0, 0, 0, 0, 0 }, // 00001 - skip
+ { 0, 0, 0, 0, 0 }, // 00010 - single var
+ { 0, 0, 0, 0, 0 }, // 00011 - skip
+ { 0, 0, 0, 0, 0 }, // 00100 - single var
+ { 0, 2, 1, 3, 4 }, // 00101
+ { 2, 0, 1, 3, 4 }, // 00110
+ { 0, 0, 0, 0, 0 }, // 00111 - skip
+ { 0, 0, 0, 0, 0 }, // 01000 - single var
+ { 0, 2, 3, 1, 4 }, // 01001
+ { 2, 0, 3, 1, 4 }, // 01010
+ { 0, 1, 3, 2, 4 }, // 01011
+ { 2, 3, 0, 1, 4 }, // 01100
+ { 0, 3, 1, 2, 4 }, // 01101
+ { 3, 0, 1, 2, 4 }, // 01110
+ { 0, 0, 0, 0, 0 }, // 01111 - skip
+ { 0, 0, 0, 0, 0 }, // 10000 - single var
+ { 0, 4, 2, 3, 1 }, // 10001
+ { 4, 0, 2, 3, 1 }, // 10010
+ { 0, 1, 3, 4, 2 }, // 10011
+ { 2, 3, 0, 4, 1 }, // 10100
+ { 0, 3, 1, 4, 2 }, // 10101
+ { 3, 0, 1, 4, 2 }, // 10110
+ { 0, 1, 2, 4, 3 }, // 10111 - four var
+ { 2, 3, 4, 0, 1 }, // 11000
+ { 0, 3, 4, 1, 2 }, // 11001
+ { 3, 0, 4, 1, 2 }, // 11010
+ { 0, 1, 4, 2, 3 }, // 11011 - four var
+ { 3, 4, 0, 1, 2 }, // 11100
+ { 0, 4, 1, 2, 3 }, // 11101 - four var
+ { 4, 0, 1, 2, 3 }, // 11110 - four var
+ { 0, 0, 0, 0, 0 } // 11111 - skip
+ };
+ int i, k, iRes;
+ unsigned uTruthRes;
+ assert( Phase >= 0 && Phase < 32 );
+ if ( Cases[Phase] == 0 )
+ return uTruth;
+ if ( Cases[Phase] > 1 )
+ return Cases[Phase];
+ uTruthRes = 0;
+ for ( i = 0; i < 32; i++ )
+ if ( uTruth & (1 << i) )
+ {
+ for ( iRes = 0, k = 0; k < 5; k++ )
+ if ( i & (1 << Perms[Phase][k]) )
+ iRes |= (1 << k);
+ uTruthRes |= (1 << iRes);
+ }
+ return uTruthRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Allocated lookup table for truth table permutation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned short ** Extra_TruthPerm43()
+{
+ unsigned short ** pTable;
+ unsigned uTruth;
+ int i, k;
+ pTable = (unsigned short **)Extra_ArrayAlloc( 256, 16, 2 );
+ for ( i = 0; i < 256; i++ )
+ {
+ uTruth = (i << 8) | i;
+ for ( k = 0; k < 16; k++ )
+ pTable[i][k] = Extra_TruthPerm4One( uTruth, k );
+ }
+ return pTable;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Allocated lookup table for truth table permutation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned ** Extra_TruthPerm53()
+{
+ unsigned ** pTable;
+ unsigned uTruth;
+ int i, k;
+ pTable = (unsigned **)Extra_ArrayAlloc( 256, 32, 4 );
+ for ( i = 0; i < 256; i++ )
+ {
+ uTruth = (i << 24) | (i << 16) | (i << 8) | i;
+ for ( k = 0; k < 32; k++ )
+ pTable[i][k] = Extra_TruthPerm5One( uTruth, k );
+ }
+ return pTable;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Allocated lookup table for truth table permutation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned ** Extra_TruthPerm54()
+{
+ unsigned ** pTable;
+ unsigned uTruth;
+ int i;
+ pTable = (unsigned **)Extra_ArrayAlloc( 256*256, 4, 4 );
+ for ( i = 0; i < 256*256; i++ )
+ {
+ uTruth = (i << 16) | i;
+ pTable[i][0] = Extra_TruthPerm5One( uTruth, 31-8 );
+ pTable[i][1] = Extra_TruthPerm5One( uTruth, 31-4 );
+ pTable[i][2] = Extra_TruthPerm5One( uTruth, 31-2 );
+ pTable[i][3] = Extra_TruthPerm5One( uTruth, 31-1 );
+ }
+ return pTable;
}
/**Function*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-06 09:41:08 +0000