summaryrefslogtreecommitdiffstats
path: root/src/misc
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc')
-rw-r--r--src/misc/extra/extra.h9
-rw-r--r--src/misc/extra/extraUtilCanon.c699
-rw-r--r--src/misc/extra/extraUtilMisc.c302
-rw-r--r--src/misc/extra/module.make1
-rw-r--r--src/misc/vec/vecInt.h2
5 files changed, 1010 insertions, 3 deletions
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 92e631ad..d298a204 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -216,6 +216,10 @@ extern unsigned Extra_TruthCanonNPN( unsigned uTruth, int nVars );
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 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 );
+/* precomputing tables for permutation mapping */
extern void ** Extra_ArrayAlloc( int nCols, int nRows, int Size );
extern unsigned short ** Extra_TruthPerm43();
extern unsigned ** Extra_TruthPerm53();
@@ -223,6 +227,11 @@ extern unsigned ** Extra_TruthPerm54();
/* for independence from CUDD */
extern unsigned int Cudd_PrimeCopy( unsigned int p );
+/*=== extraUtilCanon.c ========================================================*/
+
+/* fast computation of N-canoninical form up to 6 inputs */
+extern int Extra_TruthCanonFastN( int nVarsMax, int nVarsReal, unsigned * pt, unsigned ** pptRes, char ** ppfRes );
+
/*=== extraUtilProgress.c ================================================================*/
typedef struct ProgressBarStruct ProgressBar;
diff --git a/src/misc/extra/extraUtilCanon.c b/src/misc/extra/extraUtilCanon.c
new file mode 100644
index 00000000..9d4e5b5d
--- /dev/null
+++ b/src/misc/extra/extraUtilCanon.c
@@ -0,0 +1,699 @@
+/**CFile****************************************************************
+
+ FileName [extraUtilMisc.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [extra]
+
+ Synopsis [Computing canonical forms of Boolean functions using truth tables.]
+
+ 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_Truths3[256];
+static char s_Phases3[256][9];
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes */
+/*---------------------------------------------------------------------------*/
+
+static int Extra_TruthCanonN_rec( int nVars, unsigned char * pt, unsigned ** pptRes, char ** ppfRes, int Flag );
+
+/**AutomaticEnd***************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+ Synopsis [Computes the N-canonical form of the Boolean function up to 6 inputs.]
+
+ Description [The N-canonical form is defined as the truth table with
+ the minimum integer value. This function exhaustively enumerates
+ through the complete set of 2^N phase assignments.
+ Returns pointers to the static storage to the truth table and phases.
+ This data should be used before the function is called again.]
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Extra_TruthCanonFastN( int nVarsMax, int nVarsReal, unsigned * pt, unsigned ** pptRes, char ** ppfRes )
+{
+ static unsigned uTruthStore6[2];
+ int RetValue;
+ assert( nVarsMax <= 6 );
+ assert( nVarsReal <= nVarsMax );
+ RetValue = Extra_TruthCanonN_rec( nVarsReal <= 3? 3: nVarsReal, (unsigned char *)pt, pptRes, ppfRes, 0 );
+ if ( nVarsMax == 6 && nVarsReal < nVarsMax )
+ {
+ uTruthStore6[0] = **pptRes;
+ uTruthStore6[1] = **pptRes;
+ *pptRes = uTruthStore6;
+ }
+ return RetValue;
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions */
+/*---------------------------------------------------------------------------*/
+
+/**Function*************************************************************
+
+ Synopsis [Recursive implementation of the above.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Extra_TruthCanonN_rec( int nVars, unsigned char * pt, unsigned ** pptRes, char ** ppfRes, int Flag )
+{
+ static unsigned uTruthStore[7][2][2];
+ static char uPhaseStore[7][2][64];
+
+ unsigned char * pt0, * pt1;
+ unsigned * ptRes0, * ptRes1, * ptRes;
+ unsigned uInit0, uInit1, uTruth0, uTruth1, uTemp;
+ char * pfRes0, * pfRes1, * pfRes;
+ int nf0, nf1, nfRes, i, nVarsN;
+
+ // table lookup for three vars
+ if ( nVars == 3 )
+ {
+ *pptRes = &s_Truths3[*pt];
+ *ppfRes = s_Phases3[*pt]+1;
+ return s_Phases3[*pt][0];
+ }
+
+ // number of vars for the next call
+ nVarsN = nVars-1;
+ // truth table for the next call
+ pt0 = pt;
+ pt1 = pt + (1 << nVarsN) / 8;
+ // 5-var truth tables for this call
+ uInit0 = *((unsigned *)pt0);
+ uInit1 = *((unsigned *)pt1);
+ if ( nVarsN == 3 )
+ {
+ 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 &= 0xFFFF;
+ uInit1 &= 0xFFFF;
+ uInit0 = (uInit0 << 16) | uInit0;
+ uInit1 = (uInit1 << 16) | uInit1;
+ }
+
+ // storage for truth tables and phases
+ ptRes = uTruthStore[nVars][Flag];
+ pfRes = uPhaseStore[nVars][Flag];
+
+ // solve trivial cases
+ if ( uInit1 == 0 )
+ {
+ nf0 = Extra_TruthCanonN_rec( nVarsN, pt0, &ptRes0, &pfRes0, 0 );
+ uTruth1 = uInit1;
+ uTruth0 = *ptRes0;
+ nfRes = 0;
+ for ( i = 0; i < nf0; i++ )
+ pfRes[nfRes++] = pfRes0[i];
+ goto finish;
+ }
+ if ( uInit0 == 0 )
+ {
+ nf1 = Extra_TruthCanonN_rec( nVarsN, pt1, &ptRes1, &pfRes1, 1 );
+ uTruth1 = uInit0;
+ uTruth0 = *ptRes1;
+ nfRes = 0;
+ for ( i = 0; i < nf1; i++ )
+ pfRes[nfRes++] = pfRes1[i] | (1<<nVarsN);
+ goto finish;
+ }
+
+ if ( uInit1 == 0xFFFFFFFF )
+ {
+ nf0 = Extra_TruthCanonN_rec( nVarsN, pt0, &ptRes0, &pfRes0, 0 );
+ uTruth1 = *ptRes0;
+ uTruth0 = uInit1;
+ nfRes = 0;
+ for ( i = 0; i < nf0; i++ )
+ pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
+ goto finish;
+ }
+ if ( uInit0 == 0xFFFFFFFF )
+ {
+ nf1 = Extra_TruthCanonN_rec( nVarsN, pt1, &ptRes1, &pfRes1, 1 );
+ uTruth1 = *ptRes1;
+ uTruth0 = uInit0;
+ nfRes = 0;
+ for ( i = 0; i < nf1; i++ )
+ pfRes[nfRes++] = pfRes1[i];
+ goto finish;
+ }
+
+ // solve the problem for cofactors
+ nf0 = Extra_TruthCanonN_rec( nVarsN, pt0, &ptRes0, &pfRes0, 0 );
+ nf1 = Extra_TruthCanonN_rec( nVarsN, pt1, &ptRes1, &pfRes1, 1 );
+
+ // combine the result
+ if ( *ptRes1 < *ptRes0 )
+ {
+ uTruth0 = 0xFFFFFFFF;
+ nfRes = 0;
+ for ( i = 0; i < nf1; i++ )
+ {
+ uTemp = Extra_TruthPolarize( uInit0, pfRes1[i], nVarsN );
+ if ( uTruth0 > uTemp )
+ {
+ nfRes = 0;
+ uTruth0 = uTemp;
+ pfRes[nfRes++] = pfRes1[i];
+ }
+ else if ( uTruth0 == uTemp )
+ pfRes[nfRes++] = pfRes1[i];
+ }
+ uTruth1 = *ptRes1;
+ }
+ else if ( *ptRes1 > *ptRes0 )
+ {
+ uTruth0 = 0xFFFFFFFF;
+ nfRes = 0;
+ for ( i = 0; i < nf0; i++ )
+ {
+ uTemp = Extra_TruthPolarize( uInit1, pfRes0[i], nVarsN );
+ if ( uTruth0 > uTemp )
+ {
+ nfRes = 0;
+ uTruth0 = uTemp;
+ pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
+ }
+ else if ( uTruth0 == uTemp )
+ pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
+ }
+ uTruth1 = *ptRes0;
+ }
+ else
+ {
+ assert( nf0 == nf1 );
+ nfRes = 0;
+ for ( i = 0; i < nf1; i++ )
+ pfRes[nfRes++] = pfRes1[i];
+ for ( i = 0; i < nf0; i++ )
+ pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
+ uTruth0 = Extra_TruthPolarize( uInit0, pfRes1[0], nVarsN );
+ uTruth1 = *ptRes0;
+ }
+
+finish :
+ if ( nVarsN == 3 )
+ {
+ uTruth0 &= 0xFF;
+ uTruth1 &= 0xFF;
+ uTemp = (uTruth1 << 8) | uTruth0;
+ *ptRes = (uTemp << 16) | uTemp;
+ }
+ else if ( nVarsN == 4 )
+ {
+ uTruth0 &= 0xFFFF;
+ uTruth1 &= 0xFFFF;
+ *ptRes = (uTruth1 << 16) | uTruth0;
+ }
+ else if ( nVarsN == 5 )
+ {
+ *(ptRes+0) = uTruth0;
+ *(ptRes+1) = uTruth1;
+ }
+
+ *pptRes = ptRes;
+ *ppfRes = pfRes;
+ return nfRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Map_Var3Print()
+{
+ extern void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounters );
+
+ unsigned * uCanons;
+ char ** uPhases;
+ char * pCounters;
+ int i, k;
+
+ Extra_Truth3VarN( &uCanons, &uPhases, &pCounters );
+
+ for ( i = 0; i < 256; i++ )
+ {
+ if ( i % 8 == 0 )
+ printf( "\n" );
+ Extra_PrintHex( stdout, uCanons[i], 5 );
+ printf( ", " );
+ }
+ printf( "\n" );
+
+ for ( i = 0; i < 256; i++ )
+ {
+ printf( "%3d */ { %2d, ", i, pCounters[i] );
+ for ( k = 0; k < pCounters[i]; k++ )
+ printf( "%s%d", k? ", ":"", uPhases[i][k] );
+ printf( " }\n" );
+ }
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Map_Var3Test()
+{
+ extern void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounters );
+
+ unsigned * uCanons;
+ char ** uPhases;
+ char * pCounters;
+ int i;
+ unsigned * ptRes;
+ char * pfRes;
+ unsigned uTruth;
+ int Count;
+
+ Extra_Truth3VarN( &uCanons, &uPhases, &pCounters );
+
+ for ( i = 0; i < 256; i++ )
+ {
+ uTruth = i;
+ Count = Extra_TruthCanonFastN( 5, 3, &uTruth, &ptRes, &pfRes );
+ if ( *ptRes != uCanons[i] || Count != pCounters[i] )
+ {
+ int k = 0;
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Map_Var4Test()
+{
+ extern void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** ppCounters, int PhaseMax );
+
+ unsigned short * uCanons;
+ char ** uPhases;
+ char * pCounters;
+ int i, k;
+ unsigned * ptRes;
+ char * pfRes;
+ unsigned uTruth;
+ int Count;
+
+ Extra_Truth4VarN( &uCanons, &uPhases, &pCounters, 16 );
+
+ for ( i = 0; i < 256*256; i++ )
+ {
+ uTruth = i;
+ Count = Extra_TruthCanonFastN( 5, 4, &uTruth, &ptRes, &pfRes );
+ if ( (*ptRes & 0xFFFF) != uCanons[i] || Count != pCounters[i] )
+ {
+ int k = 0;
+ }
+ for ( k = 0; k < Count; k++ )
+ if ( uPhases[i][k] != pfRes[k] )
+ {
+ int v = 0;
+ }
+ }
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static Functions */
+/*---------------------------------------------------------------------------*/
+
+static unsigned s_Truths3[256] =
+{
+ 0x00000000, 0x01010101, 0x01010101, 0x03030303, 0x01010101, 0x05050505, 0x06060606, 0x07070707,
+ 0x01010101, 0x06060606, 0x05050505, 0x07070707, 0x03030303, 0x07070707, 0x07070707, 0x0f0f0f0f,
+ 0x01010101, 0x11111111, 0x12121212, 0x13131313, 0x14141414, 0x15151515, 0x16161616, 0x17171717,
+ 0x18181818, 0x19191919, 0x1a1a1a1a, 0x1b1b1b1b, 0x1c1c1c1c, 0x1d1d1d1d, 0x1e1e1e1e, 0x1f1f1f1f,
+ 0x01010101, 0x12121212, 0x11111111, 0x13131313, 0x18181818, 0x1a1a1a1a, 0x19191919, 0x1b1b1b1b,
+ 0x14141414, 0x16161616, 0x15151515, 0x17171717, 0x1c1c1c1c, 0x1e1e1e1e, 0x1d1d1d1d, 0x1f1f1f1f,
+ 0x03030303, 0x13131313, 0x13131313, 0x33333333, 0x1c1c1c1c, 0x35353535, 0x36363636, 0x37373737,
+ 0x1c1c1c1c, 0x36363636, 0x35353535, 0x37373737, 0x3c3c3c3c, 0x3d3d3d3d, 0x3d3d3d3d, 0x3f3f3f3f,
+ 0x01010101, 0x14141414, 0x18181818, 0x1c1c1c1c, 0x11111111, 0x15151515, 0x19191919, 0x1d1d1d1d,
+ 0x12121212, 0x16161616, 0x1a1a1a1a, 0x1e1e1e1e, 0x13131313, 0x17171717, 0x1b1b1b1b, 0x1f1f1f1f,
+ 0x05050505, 0x15151515, 0x1a1a1a1a, 0x35353535, 0x15151515, 0x55555555, 0x56565656, 0x57575757,
+ 0x1a1a1a1a, 0x56565656, 0x5a5a5a5a, 0x5b5b5b5b, 0x35353535, 0x57575757, 0x5b5b5b5b, 0x5f5f5f5f,
+ 0x06060606, 0x16161616, 0x19191919, 0x36363636, 0x19191919, 0x56565656, 0x66666666, 0x67676767,
+ 0x16161616, 0x69696969, 0x56565656, 0x6b6b6b6b, 0x36363636, 0x6b6b6b6b, 0x67676767, 0x6f6f6f6f,
+ 0x07070707, 0x17171717, 0x1b1b1b1b, 0x37373737, 0x1d1d1d1d, 0x57575757, 0x67676767, 0x77777777,
+ 0x1e1e1e1e, 0x6b6b6b6b, 0x5b5b5b5b, 0x7b7b7b7b, 0x3d3d3d3d, 0x7d7d7d7d, 0x7e7e7e7e, 0x7f7f7f7f,
+ 0x01010101, 0x18181818, 0x14141414, 0x1c1c1c1c, 0x12121212, 0x1a1a1a1a, 0x16161616, 0x1e1e1e1e,
+ 0x11111111, 0x19191919, 0x15151515, 0x1d1d1d1d, 0x13131313, 0x1b1b1b1b, 0x17171717, 0x1f1f1f1f,
+ 0x06060606, 0x19191919, 0x16161616, 0x36363636, 0x16161616, 0x56565656, 0x69696969, 0x6b6b6b6b,
+ 0x19191919, 0x66666666, 0x56565656, 0x67676767, 0x36363636, 0x67676767, 0x6b6b6b6b, 0x6f6f6f6f,
+ 0x05050505, 0x1a1a1a1a, 0x15151515, 0x35353535, 0x1a1a1a1a, 0x5a5a5a5a, 0x56565656, 0x5b5b5b5b,
+ 0x15151515, 0x56565656, 0x55555555, 0x57575757, 0x35353535, 0x5b5b5b5b, 0x57575757, 0x5f5f5f5f,
+ 0x07070707, 0x1b1b1b1b, 0x17171717, 0x37373737, 0x1e1e1e1e, 0x5b5b5b5b, 0x6b6b6b6b, 0x7b7b7b7b,
+ 0x1d1d1d1d, 0x67676767, 0x57575757, 0x77777777, 0x3d3d3d3d, 0x7e7e7e7e, 0x7d7d7d7d, 0x7f7f7f7f,
+ 0x03030303, 0x1c1c1c1c, 0x1c1c1c1c, 0x3c3c3c3c, 0x13131313, 0x35353535, 0x36363636, 0x3d3d3d3d,
+ 0x13131313, 0x36363636, 0x35353535, 0x3d3d3d3d, 0x33333333, 0x37373737, 0x37373737, 0x3f3f3f3f,
+ 0x07070707, 0x1d1d1d1d, 0x1e1e1e1e, 0x3d3d3d3d, 0x17171717, 0x57575757, 0x6b6b6b6b, 0x7d7d7d7d,
+ 0x1b1b1b1b, 0x67676767, 0x5b5b5b5b, 0x7e7e7e7e, 0x37373737, 0x77777777, 0x7b7b7b7b, 0x7f7f7f7f,
+ 0x07070707, 0x1e1e1e1e, 0x1d1d1d1d, 0x3d3d3d3d, 0x1b1b1b1b, 0x5b5b5b5b, 0x67676767, 0x7e7e7e7e,
+ 0x17171717, 0x6b6b6b6b, 0x57575757, 0x7d7d7d7d, 0x37373737, 0x7b7b7b7b, 0x77777777, 0x7f7f7f7f,
+ 0x0f0f0f0f, 0x1f1f1f1f, 0x1f1f1f1f, 0x3f3f3f3f, 0x1f1f1f1f, 0x5f5f5f5f, 0x6f6f6f6f, 0x7f7f7f7f,
+ 0x1f1f1f1f, 0x6f6f6f6f, 0x5f5f5f5f, 0x7f7f7f7f, 0x3f3f3f3f, 0x7f7f7f7f, 0x7f7f7f7f, 0xffffffff
+};
+
+static char s_Phases3[256][9] =
+{
+/* 0 */ { 8, 0, 1, 2, 3, 4, 5, 6, 7 },
+/* 1 */ { 1, 0 },
+/* 2 */ { 1, 1 },
+/* 3 */ { 2, 0, 1 },
+/* 4 */ { 1, 2 },
+/* 5 */ { 2, 0, 2 },
+/* 6 */ { 2, 0, 3 },
+/* 7 */ { 1, 0 },
+/* 8 */ { 1, 3 },
+/* 9 */ { 2, 1, 2 },
+/* 10 */ { 2, 1, 3 },
+/* 11 */ { 1, 1 },
+/* 12 */ { 2, 2, 3 },
+/* 13 */ { 1, 2 },
+/* 14 */ { 1, 3 },
+/* 15 */ { 4, 0, 1, 2, 3 },
+/* 16 */ { 1, 4 },
+/* 17 */ { 2, 0, 4 },
+/* 18 */ { 2, 0, 5 },
+/* 19 */ { 1, 0 },
+/* 20 */ { 2, 0, 6 },
+/* 21 */ { 1, 0 },
+/* 22 */ { 1, 0 },
+/* 23 */ { 1, 0 },
+/* 24 */ { 2, 0, 7 },
+/* 25 */ { 1, 0 },
+/* 26 */ { 1, 0 },
+/* 27 */ { 1, 0 },
+/* 28 */ { 1, 0 },
+/* 29 */ { 1, 0 },
+/* 30 */ { 1, 0 },
+/* 31 */ { 1, 0 },
+/* 32 */ { 1, 5 },
+/* 33 */ { 2, 1, 4 },
+/* 34 */ { 2, 1, 5 },
+/* 35 */ { 1, 1 },
+/* 36 */ { 2, 1, 6 },
+/* 37 */ { 1, 1 },
+/* 38 */ { 1, 1 },
+/* 39 */ { 1, 1 },
+/* 40 */ { 2, 1, 7 },
+/* 41 */ { 1, 1 },
+/* 42 */ { 1, 1 },
+/* 43 */ { 1, 1 },
+/* 44 */ { 1, 1 },
+/* 45 */ { 1, 1 },
+/* 46 */ { 1, 1 },
+/* 47 */ { 1, 1 },
+/* 48 */ { 2, 4, 5 },
+/* 49 */ { 1, 4 },
+/* 50 */ { 1, 5 },
+/* 51 */ { 4, 0, 1, 4, 5 },
+/* 52 */ { 1, 6 },
+/* 53 */ { 1, 0 },
+/* 54 */ { 1, 0 },
+/* 55 */ { 1, 0 },
+/* 56 */ { 1, 7 },
+/* 57 */ { 1, 1 },
+/* 58 */ { 1, 1 },
+/* 59 */ { 1, 1 },
+/* 60 */ { 4, 0, 1, 6, 7 },
+/* 61 */ { 1, 0 },
+/* 62 */ { 1, 1 },
+/* 63 */ { 2, 0, 1 },
+/* 64 */ { 1, 6 },
+/* 65 */ { 2, 2, 4 },
+/* 66 */ { 2, 2, 5 },
+/* 67 */ { 1, 2 },
+/* 68 */ { 2, 2, 6 },
+/* 69 */ { 1, 2 },
+/* 70 */ { 1, 2 },
+/* 71 */ { 1, 2 },
+/* 72 */ { 2, 2, 7 },
+/* 73 */ { 1, 2 },
+/* 74 */ { 1, 2 },
+/* 75 */ { 1, 2 },
+/* 76 */ { 1, 2 },
+/* 77 */ { 1, 2 },
+/* 78 */ { 1, 2 },
+/* 79 */ { 1, 2 },
+/* 80 */ { 2, 4, 6 },
+/* 81 */ { 1, 4 },
+/* 82 */ { 1, 5 },
+/* 83 */ { 1, 4 },
+/* 84 */ { 1, 6 },
+/* 85 */ { 4, 0, 2, 4, 6 },
+/* 86 */ { 1, 0 },
+/* 87 */ { 1, 0 },
+/* 88 */ { 1, 7 },
+/* 89 */ { 1, 2 },
+/* 90 */ { 4, 0, 2, 5, 7 },
+/* 91 */ { 1, 0 },
+/* 92 */ { 1, 6 },
+/* 93 */ { 1, 2 },
+/* 94 */ { 1, 2 },
+/* 95 */ { 2, 0, 2 },
+/* 96 */ { 2, 4, 7 },
+/* 97 */ { 1, 4 },
+/* 98 */ { 1, 5 },
+/* 99 */ { 1, 4 },
+/* 100 */ { 1, 6 },
+/* 101 */ { 1, 4 },
+/* 102 */ { 4, 0, 3, 4, 7 },
+/* 103 */ { 1, 0 },
+/* 104 */ { 1, 7 },
+/* 105 */ { 4, 0, 3, 5, 6 },
+/* 106 */ { 1, 7 },
+/* 107 */ { 1, 0 },
+/* 108 */ { 1, 7 },
+/* 109 */ { 1, 3 },
+/* 110 */ { 1, 3 },
+/* 111 */ { 2, 0, 3 },
+/* 112 */ { 1, 4 },
+/* 113 */ { 1, 4 },
+/* 114 */ { 1, 5 },
+/* 115 */ { 1, 4 },
+/* 116 */ { 1, 6 },
+/* 117 */ { 1, 4 },
+/* 118 */ { 1, 4 },
+/* 119 */ { 2, 0, 4 },
+/* 120 */ { 1, 7 },
+/* 121 */ { 1, 5 },
+/* 122 */ { 1, 5 },
+/* 123 */ { 2, 0, 5 },
+/* 124 */ { 1, 6 },
+/* 125 */ { 2, 0, 6 },
+/* 126 */ { 2, 0, 7 },
+/* 127 */ { 1, 0 },
+/* 128 */ { 1, 7 },
+/* 129 */ { 2, 3, 4 },
+/* 130 */ { 2, 3, 5 },
+/* 131 */ { 1, 3 },
+/* 132 */ { 2, 3, 6 },
+/* 133 */ { 1, 3 },
+/* 134 */ { 1, 3 },
+/* 135 */ { 1, 3 },
+/* 136 */ { 2, 3, 7 },
+/* 137 */ { 1, 3 },
+/* 138 */ { 1, 3 },
+/* 139 */ { 1, 3 },
+/* 140 */ { 1, 3 },
+/* 141 */ { 1, 3 },
+/* 142 */ { 1, 3 },
+/* 143 */ { 1, 3 },
+/* 144 */ { 2, 5, 6 },
+/* 145 */ { 1, 4 },
+/* 146 */ { 1, 5 },
+/* 147 */ { 1, 5 },
+/* 148 */ { 1, 6 },
+/* 149 */ { 1, 6 },
+/* 150 */ { 4, 1, 2, 4, 7 },
+/* 151 */ { 1, 1 },
+/* 152 */ { 1, 7 },
+/* 153 */ { 4, 1, 2, 5, 6 },
+/* 154 */ { 1, 5 },
+/* 155 */ { 1, 1 },
+/* 156 */ { 1, 6 },
+/* 157 */ { 1, 2 },
+/* 158 */ { 1, 2 },
+/* 159 */ { 2, 1, 2 },
+/* 160 */ { 2, 5, 7 },
+/* 161 */ { 1, 4 },
+/* 162 */ { 1, 5 },
+/* 163 */ { 1, 5 },
+/* 164 */ { 1, 6 },
+/* 165 */ { 4, 1, 3, 4, 6 },
+/* 166 */ { 1, 3 },
+/* 167 */ { 1, 1 },
+/* 168 */ { 1, 7 },
+/* 169 */ { 1, 1 },
+/* 170 */ { 4, 1, 3, 5, 7 },
+/* 171 */ { 1, 1 },
+/* 172 */ { 1, 7 },
+/* 173 */ { 1, 3 },
+/* 174 */ { 1, 3 },
+/* 175 */ { 2, 1, 3 },
+/* 176 */ { 1, 5 },
+/* 177 */ { 1, 4 },
+/* 178 */ { 1, 5 },
+/* 179 */ { 1, 5 },
+/* 180 */ { 1, 6 },
+/* 181 */ { 1, 4 },
+/* 182 */ { 1, 4 },
+/* 183 */ { 2, 1, 4 },
+/* 184 */ { 1, 7 },
+/* 185 */ { 1, 5 },
+/* 186 */ { 1, 5 },
+/* 187 */ { 2, 1, 5 },
+/* 188 */ { 1, 7 },
+/* 189 */ { 2, 1, 6 },
+/* 190 */ { 2, 1, 7 },
+/* 191 */ { 1, 1 },
+/* 192 */ { 2, 6, 7 },
+/* 193 */ { 1, 4 },
+/* 194 */ { 1, 5 },
+/* 195 */ { 4, 2, 3, 4, 5 },
+/* 196 */ { 1, 6 },
+/* 197 */ { 1, 2 },
+/* 198 */ { 1, 3 },
+/* 199 */ { 1, 2 },
+/* 200 */ { 1, 7 },
+/* 201 */ { 1, 2 },
+/* 202 */ { 1, 3 },
+/* 203 */ { 1, 3 },
+/* 204 */ { 4, 2, 3, 6, 7 },
+/* 205 */ { 1, 2 },
+/* 206 */ { 1, 3 },
+/* 207 */ { 2, 2, 3 },
+/* 208 */ { 1, 6 },
+/* 209 */ { 1, 4 },
+/* 210 */ { 1, 5 },
+/* 211 */ { 1, 4 },
+/* 212 */ { 1, 6 },
+/* 213 */ { 1, 6 },
+/* 214 */ { 1, 7 },
+/* 215 */ { 2, 2, 4 },
+/* 216 */ { 1, 7 },
+/* 217 */ { 1, 6 },
+/* 218 */ { 1, 7 },
+/* 219 */ { 2, 2, 5 },
+/* 220 */ { 1, 6 },
+/* 221 */ { 2, 2, 6 },
+/* 222 */ { 2, 2, 7 },
+/* 223 */ { 1, 2 },
+/* 224 */ { 1, 7 },
+/* 225 */ { 1, 4 },
+/* 226 */ { 1, 5 },
+/* 227 */ { 1, 5 },
+/* 228 */ { 1, 6 },
+/* 229 */ { 1, 6 },
+/* 230 */ { 1, 7 },
+/* 231 */ { 2, 3, 4 },
+/* 232 */ { 1, 7 },
+/* 233 */ { 1, 6 },
+/* 234 */ { 1, 7 },
+/* 235 */ { 2, 3, 5 },
+/* 236 */ { 1, 7 },
+/* 237 */ { 2, 3, 6 },
+/* 238 */ { 2, 3, 7 },
+/* 239 */ { 1, 3 },
+/* 240 */ { 4, 4, 5, 6, 7 },
+/* 241 */ { 1, 4 },
+/* 242 */ { 1, 5 },
+/* 243 */ { 2, 4, 5 },
+/* 244 */ { 1, 6 },
+/* 245 */ { 2, 4, 6 },
+/* 246 */ { 2, 4, 7 },
+/* 247 */ { 1, 4 },
+/* 248 */ { 1, 7 },
+/* 249 */ { 2, 5, 6 },
+/* 250 */ { 2, 5, 7 },
+/* 251 */ { 1, 5 },
+/* 252 */ { 2, 6, 7 },
+/* 253 */ { 1, 6 },
+/* 254 */ { 1, 7 },
+/* 255 */ { 8, 0, 1, 2, 3, 4, 5, 6, 7 }
+};
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index 2767498b..a12fbce4 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -429,8 +429,6 @@ unsigned Extra_TruthPolarize( unsigned uTruth, int Polarity, int nVars )
uCof1 >>= Shift;
uTruth = uCof0 | uCof1;
}
- if ( nVars < 5 )
- uTruth &= ((~0) >> (32-nMints));
return uTruth;
}
@@ -752,6 +750,74 @@ void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** p
SeeAlso []
***********************************************************************/
+void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounters )
+{
+ int nPhasesMax = 8;
+ unsigned * uCanons;
+ unsigned uTruth, uPhase, uTruth32;
+ char ** uPhases, * pCounters;
+ int nFuncs, nClasses, i;
+
+ nFuncs = (1 << 8);
+ uCanons = ALLOC( unsigned, nFuncs );
+ memset( uCanons, 0, sizeof(unsigned) * 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
+ uTruth32 = ((uTruth << 24) | (uTruth << 16) | (uTruth << 8) | uTruth);
+ if ( uCanons[uTruth] )
+ {
+ assert( uTruth32 > uCanons[uTruth] );
+ continue;
+ }
+ nClasses++;
+ for ( i = 0; i < 8; i++ )
+ {
+ uPhase = Extra_TruthPolarize( uTruth, i, 3 );
+ if ( uCanons[uPhase] == 0 && (uTruth || i==0) )
+ {
+ uCanons[uPhase] = uTruth32;
+ uPhases[uPhase][0] = i;
+ pCounters[uPhase] = 1;
+ }
+ else
+ {
+ assert( uCanons[uPhase] == uTruth32 );
+ 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 );
+ printf( "The number of 3N-classes = %d.\n", nClasses );
+}
+
+/**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;
@@ -778,7 +844,7 @@ void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** pp
for ( i = 0; i < 16; i++ )
{
uPhase = Extra_TruthPolarize( uTruth, i, 4 );
- if ( uCanons[uPhase] == 0 )
+ if ( uCanons[uPhase] == 0 && (uTruth || i==0) )
{
uCanons[uPhase] = uTruth;
uPhases[uPhase][0] = i;
@@ -804,6 +870,7 @@ void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** pp
*ppCounters = pCounters;
else
free( pCounters );
+ printf( "The number of 4N-classes = %d.\n", nClasses );
}
/**Function*************************************************************
@@ -1005,6 +1072,208 @@ unsigned Extra_TruthPerm5One( unsigned uTruth, int Phase )
/**Function*************************************************************
+ Synopsis [Computes a phase of the 3-var function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_TruthPerm6One( unsigned * uTruth, int Phase, unsigned * uTruthRes )
+{
+ // cases
+ static unsigned Cases[64] = {
+ 0, // 000000 - skip
+ 0, // 000001 - skip
+ 0xCCCCCCCC, // 000010 - single var
+ 0, // 000011 - skip
+ 0xF0F0F0F0, // 000100 - single var
+ 1, // 000101
+ 1, // 000110
+ 0, // 000111 - skip
+ 0xFF00FF00, // 001000 - single var
+ 1, // 001001
+ 1, // 001010
+ 1, // 001011
+ 1, // 001100
+ 1, // 001101
+ 1, // 001110
+ 0, // 001111 - skip
+ 0xFFFF0000, // 010000 - skip
+ 1, // 010001
+ 1, // 010010
+ 1, // 010011
+ 1, // 010100
+ 1, // 010101
+ 1, // 010110
+ 1, // 010111 - four var
+ 1, // 011000
+ 1, // 011001
+ 1, // 011010
+ 1, // 011011 - four var
+ 1, // 011100
+ 1, // 011101 - four var
+ 1, // 011110 - four var
+ 0, // 011111 - skip
+ 0xFFFFFFFF, // 100000 - single var
+ 1, // 100001
+ 1, // 100010
+ 1, // 100011
+ 1, // 100100
+ 1, // 100101
+ 1, // 100110
+ 1, // 100111
+ 1, // 101000
+ 1, // 101001
+ 1, // 101010
+ 1, // 101011
+ 1, // 101100
+ 1, // 101101
+ 1, // 101110
+ 1, // 101111
+ 1, // 110000
+ 1, // 110001
+ 1, // 110010
+ 1, // 110011
+ 1, // 110100
+ 1, // 110101
+ 1, // 110110
+ 1, // 110111
+ 1, // 111000
+ 1, // 111001
+ 1, // 111010
+ 1, // 111011
+ 1, // 111100
+ 1, // 111101
+ 1, // 111110
+ 0 // 111111 - skip
+ };
+ // permutations
+ static int Perms[64][6] = {
+ { 0, 0, 0, 0, 0, 0 }, // 000000 - skip
+ { 0, 0, 0, 0, 0, 0 }, // 000001 - skip
+ { 0, 0, 0, 0, 0, 0 }, // 000010 - single var
+ { 0, 0, 0, 0, 0, 0 }, // 000011 - skip
+ { 0, 0, 0, 0, 0, 0 }, // 000100 - single var
+ { 0, 2, 1, 3, 4, 5 }, // 000101
+ { 2, 0, 1, 3, 4, 5 }, // 000110
+ { 0, 0, 0, 0, 0, 0 }, // 000111 - skip
+ { 0, 0, 0, 0, 0, 0 }, // 001000 - single var
+ { 0, 2, 3, 1, 4, 5 }, // 001001
+ { 2, 0, 3, 1, 4, 5 }, // 001010
+ { 0, 1, 3, 2, 4, 5 }, // 001011
+ { 2, 3, 0, 1, 4, 5 }, // 001100
+ { 0, 3, 1, 2, 4, 5 }, // 001101
+ { 3, 0, 1, 2, 4, 5 }, // 001110
+ { 0, 0, 0, 0, 0, 0 }, // 001111 - skip
+ { 0, 0, 0, 0, 0, 0 }, // 010000 - skip
+ { 0, 4, 2, 3, 1, 5 }, // 010001
+ { 4, 0, 2, 3, 1, 5 }, // 010010
+ { 0, 1, 3, 4, 2, 5 }, // 010011
+ { 2, 3, 0, 4, 1, 5 }, // 010100
+ { 0, 3, 1, 4, 2, 5 }, // 010101
+ { 3, 0, 1, 4, 2, 5 }, // 010110
+ { 0, 1, 2, 4, 3, 5 }, // 010111 - four var
+ { 2, 3, 4, 0, 1, 5 }, // 011000
+ { 0, 3, 4, 1, 2, 5 }, // 011001
+ { 3, 0, 4, 1, 2, 5 }, // 011010
+ { 0, 1, 4, 2, 3, 5 }, // 011011 - four var
+ { 3, 4, 0, 1, 2, 5 }, // 011100
+ { 0, 4, 1, 2, 3, 5 }, // 011101 - four var
+ { 4, 0, 1, 2, 3, 5 }, // 011110 - four var
+ { 0, 0, 0, 0, 0, 0 }, // 011111 - skip
+ { 0, 0, 0, 0, 0, 0 }, // 100000 - single var
+ { 0, 2, 3, 4, 5, 1 }, // 100001
+ { 2, 0, 3, 4, 5, 1 }, // 100010
+ { 0, 1, 3, 4, 5, 2 }, // 100011
+ { 2, 3, 0, 4, 5, 1 }, // 100100
+ { 0, 3, 1, 4, 5, 2 }, // 100101
+ { 3, 0, 1, 4, 5, 2 }, // 100110
+ { 0, 1, 2, 4, 5, 3 }, // 100111
+ { 2, 3, 4, 0, 5, 1 }, // 101000
+ { 0, 3, 4, 1, 5, 2 }, // 101001
+ { 3, 0, 4, 1, 5, 2 }, // 101010
+ { 0, 1, 4, 2, 5, 3 }, // 101011
+ { 3, 4, 0, 1, 5, 2 }, // 101100
+ { 0, 4, 1, 2, 5, 3 }, // 101101
+ { 4, 0, 1, 2, 5, 3 }, // 101110
+ { 0, 1, 2, 3, 5, 4 }, // 101111
+ { 2, 3, 4, 5, 0, 1 }, // 110000
+ { 0, 3, 4, 5, 1, 2 }, // 110001
+ { 3, 0, 4, 5, 1, 2 }, // 110010
+ { 0, 1, 4, 5, 2, 3 }, // 110011
+ { 3, 4, 0, 5, 1, 2 }, // 110100
+ { 0, 4, 1, 5, 2, 3 }, // 110101
+ { 4, 0, 1, 5, 2, 3 }, // 110110
+ { 0, 1, 2, 5, 3, 4 }, // 110111
+ { 3, 4, 5, 0, 1, 2 }, // 111000
+ { 0, 4, 5, 1, 2, 3 }, // 111001
+ { 4, 0, 5, 1, 2, 3 }, // 111010
+ { 0, 1, 5, 2, 3, 4 }, // 111011
+ { 4, 5, 0, 1, 2, 3 }, // 111100
+ { 0, 5, 1, 2, 3, 4 }, // 111101
+ { 5, 0, 1, 2, 3, 4 }, // 111110
+ { 0, 0, 0, 0, 0, 0 } // 111111 - skip
+ };
+ int i, k, iRes;
+ assert( Phase >= 0 && Phase < 64 );
+ if ( Cases[Phase] == 0 )
+ {
+ uTruthRes[0] = uTruth[0];
+ uTruthRes[1] = uTruth[1];
+ return;
+ }
+ if ( Cases[Phase] > 1 )
+ {
+ if ( Phase == 32 )
+ {
+ uTruthRes[0] = 0x00000000;
+ uTruthRes[1] = 0xFFFFFFFF;
+ }
+ else
+ {
+ uTruthRes[0] = Cases[Phase];
+ uTruthRes[1] = Cases[Phase];
+ }
+ return;
+ }
+ uTruthRes[0] = 0;
+ uTruthRes[1] = 0;
+ for ( i = 0; i < 64; i++ )
+ {
+ if ( i < 32 )
+ {
+ if ( uTruth[0] & (1 << i) )
+ {
+ for ( iRes = 0, k = 0; k < 6; k++ )
+ if ( i & (1 << Perms[Phase][k]) )
+ iRes |= (1 << k);
+ if ( iRes < 32 )
+ uTruthRes[0] |= (1 << iRes);
+ else
+ uTruthRes[1] |= (1 << (iRes-32));
+ }
+ }
+ else
+ {
+ if ( uTruth[1] & (1 << (i-32)) )
+ {
+ for ( iRes = 0, k = 0; k < 6; k++ )
+ if ( i & (1 << Perms[Phase][k]) )
+ iRes |= (1 << k);
+ if ( iRes < 32 )
+ uTruthRes[0] |= (1 << iRes);
+ else
+ uTruthRes[1] |= (1 << (iRes-32));
+ }
+ }
+ }
+}
+
+/**Function*************************************************************
+
Synopsis [Allocated lookup table for truth table permutation.]
Description []
@@ -1085,6 +1354,33 @@ unsigned ** Extra_TruthPerm54()
/**Function*************************************************************
+ Synopsis [Allocated lookup table for truth table permutation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned ** Extra_TruthPerm63()
+{
+ unsigned ** pTable;
+ unsigned uTruth[2];
+ int i, k;
+ pTable = (unsigned **)Extra_ArrayAlloc( 256, 64, 8 );
+ for ( i = 0; i < 256; i++ )
+ {
+ uTruth[0] = (i << 24) | (i << 16) | (i << 8) | i;
+ uTruth[1] = uTruth[0];
+ for ( k = 0; k < 64; k++ )
+ Extra_TruthPerm6One( uTruth, k, &pTable[i][k] );
+ }
+ return pTable;
+}
+
+/**Function*************************************************************
+
Synopsis [Returns the smallest prime larger than the number.]
Description []
diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make
index bfc9d0ad..3098a23c 100644
--- a/src/misc/extra/module.make
+++ b/src/misc/extra/module.make
@@ -1,5 +1,6 @@
SRC += src/misc/extra/extraUtilBdd.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 \
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index effebc68..919b7e5a 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -50,6 +50,8 @@ struct Vec_Int_t_
#define Vec_IntForEachEntry( vVec, Entry, i ) \
for ( i = 0; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
+#define Vec_IntForEachEntryStart( vVec, Entry, i, Start ) \
+ for ( i = Start; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-17 19:07:03 +0000