Version abc70328

3 files changed, 83 insertions, 17 deletions

diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 4aa2c816..06ba309d 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -114,7 +114,7 @@ typedef unsigned long long uint64;
 #endif
 
 #ifndef PRTP
-#define PRTP(a,t,T)  printf("%s = ", (a)); printf("%6.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), 100.0*(t)/(T))
+#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
 
 /*===========================================================================*/
@@ -322,6 +322,7 @@ 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 );
 
@@ -530,22 +531,23 @@ static inline void Extra_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned *
         pOut[w] = ~(pIn0[w] & pIn1[w]);
 }
 
-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 );
+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 ================================================================*/
 
diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c
index 6b130e7e..4c51b8b5 100644
--- a/src/misc/extra/extraUtilFile.c
+++ b/src/misc/extra/extraUtilFile.c
@@ -385,6 +385,34 @@ void Extra_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars )
   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 []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Extra_PrintHex( FILE * pFile, unsigned uTruth, int nVars )
 {
     int nMints, nDigits, Digit, k;
diff --git a/src/misc/extra/extraUtilTruth.c b/src/misc/extra/extraUtilTruth.c
index 7a22545b..3b0b16eb 100644
--- a/src/misc/extra/extraUtilTruth.c
+++ b/src/misc/extra/extraUtilTruth.c
@@ -62,6 +62,42 @@ static unsigned s_VarMasks[5][2] = {
 
 /**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).