Improvements to the canonical form computation.

6 files changed, 133 insertions, 13 deletions

diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c
index 454a1b3d..252a8187 100644
--- a/src/aig/gia/giaJf.c
+++ b/src/aig/gia/giaJf.c
@@ -357,6 +357,16 @@ Jf_Man_t * Jf_ManAlloc( Gia_Man_t * pGia, Jf_Par_t * pPars )
     p->clkStart  = Abc_Clock();
     return p;
 }
+void Jf_ManDumpTruthTables( Jf_Man_t * p )
+{
+    char * pFileName = "truths.txt";
+    FILE * pFile = fopen( pFileName, "wb" );
+    Vec_MemDump( pFile, p->vTtMem );
+    fclose( pFile );
+    printf( "Dumped %d %d-var truth tables into file \"%s\" (%.2f MB).\n", 
+        Vec_MemEntryNum(p->vTtMem), p->pPars->nLutSize, pFileName,
+        17.0 * Vec_MemEntryNum(p->vTtMem) / (1 << 20) );
+}
 void Jf_ManFree( Jf_Man_t * p )
 {
     if ( p->pPars->fVerbose && p->pDsd )
@@ -365,16 +375,6 @@ void Jf_ManFree( Jf_Man_t * p )
         printf( "Unique truth tables = %d. Memory = %.2f MB\n", Vec_MemEntryNum(p->vTtMem), Vec_MemMemory(p->vTtMem) / (1<<20) ); 
     if ( p->pPars->fVeryVerbose && p->pPars->fCutMin && p->pPars->fFuncDsd )
         Jf_ManProfileClasses( p );
-    if ( p->pPars->fVeryVerbose && p->pPars->fCutMin && !p->pPars->fFuncDsd )
-    {
-        char * pFileName = "truths.txt";
-        FILE * pFile = fopen( pFileName, "wb" );
-        Vec_MemDump( pFile, p->vTtMem );
-        fclose( pFile );
-        printf( "Dumped %d %d-var truth tables into file \"%s\" (%.2f MB).\n", 
-            Vec_MemEntryNum(p->vTtMem), p->pPars->nLutSize, pFileName,
-            17.0 * Vec_MemEntryNum(p->vTtMem) / (1 << 20) );
-    }
     if ( p->pPars->fCoarsen )
         Gia_ManCleanMark0( p->pGia );
     ABC_FREE( p->pGia->pRefs );
@@ -1689,6 +1689,8 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
         Jf_ManPropagateEla( p, 0 );                 Jf_ManPrintStats( p, "Area " );
         Jf_ManPropagateEla( p, 1 );                 Jf_ManPrintStats( p, "Edge " );
     }
+    if ( p->pPars->fVeryVerbose && p->pPars->fCutMin && !p->pPars->fFuncDsd )
+        Jf_ManDumpTruthTables( p );
     if ( p->pPars->fPureAig )
         pNew = Jf_ManDeriveGia(p);
     else if ( p->pPars->fCutMin )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index dec99fc0..ad44f2e9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -5388,6 +5388,7 @@ usage:
     Abc_Print( -2, "\t               3: Jake's hybrid semi-canonical form (fast)\n" );
     Abc_Print( -2, "\t               4: Jake's hybrid semi-canonical form (high-effort)\n" );
     Abc_Print( -2, "\t               5: new fast hybrid semi-canonical form\n" );
+    Abc_Print( -2, "\t               6: new phase canonical form\n" );
     Abc_Print( -2, "\t-N <num> : the number of support variables (binary files only) [default = unused]\n" );
     Abc_Print( -2, "\t-d       : toggle dumping resulting functions into a file [default = %s]\n", fDumpRes? "yes": "no" );
     Abc_Print( -2, "\t-b       : toggle dumping in binary format [default = %s]\n", fBinary? "yes": "no" );
diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c
index 7157b856..87a00651 100644
--- a/src/base/abci/abcNpn.c
+++ b/src/base/abci/abcNpn.c
@@ -151,9 +151,12 @@ int Abc_TruthNpnCountUniqueSort( Abc_TtStore_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_TruthNpnPrint( char * pCanonPerm, unsigned uCanonPhase, int nVars )
+void Abc_TruthNpnPrint( char * pCanonPermInit, unsigned uCanonPhase, int nVars )
 {
-    int i;
+    char pCanonPerm[16]; int i;
+    assert( nVars <= 16 );
+    for ( i = 0; i < nVars; i++ )
+        pCanonPerm[i] = pCanonPermInit ? pCanonPermInit[i] : 'a' + i;
     printf( "   %c = ( ", Abc_InfoHasBit(&uCanonPhase, nVars) ? 'Z':'z' );
     for ( i = 0; i < nVars; i++ )
         printf( "%c%s", pCanonPerm[i] + ('A'-'a') * Abc_InfoHasBit(&uCanonPhase, pCanonPerm[i]-'a'), i == nVars-1 ? "":"," );
@@ -193,6 +196,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
         pAlgoName = "Jake's hybrid good ";
     else if ( NpnType == 5 )
         pAlgoName = "new hybrid fast    ";
+    else if ( NpnType == 6 )
+        pAlgoName = "new phase flipping ";
 
     assert( p->nVars <= 16 );
     if ( pAlgoName )
@@ -273,6 +278,17 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
                 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
         }
     }
+    else if ( NpnType == 6 )
+    {
+        for ( i = 0; i < p->nFuncs; i++ )
+        {
+            if ( fVerbose )
+                printf( "%7d : ", i );
+            uCanonPhase = Abc_TtCanonicizePhase( p->pFuncs[i], p->nVars );
+            if ( fVerbose )
+                Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(NULL, uCanonPhase, p->nVars), printf( "\n" );
+        }
+    }
     else assert( 0 );
     clk = Abc_Clock() - clk;
     printf( "Classes =%9d  ", Abc_TruthNpnCountUnique(p) );
@@ -336,7 +352,7 @@ int Abc_NpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes, int f
 {
     if ( fVerbose )
         printf( "Using truth tables from file \"%s\"...\n", pFileName );
-    if ( NpnType >= 0 && NpnType <= 5 )
+    if ( NpnType >= 0 && NpnType <= 6 )
         Abc_TruthNpnTest( pFileName, NpnType, nVarNum, fDumpRes, fBinary, fVerbose );
     else
         printf( "Unknown canonical form value (%d).\n", NpnType );
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 5561a2c6..7010bf2d 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -1200,6 +1200,7 @@ static inline void Abc_TtImplementNpnConfig( word * pTruth, int nVars, char * pC
     for ( i = 0; i < nVars; i++ )
         if ( (uCanonPhase >> i) & 1 )
             Abc_TtFlip( pTruth, nWords, i );
+    if ( pCanonPerm )
     for ( i = 0; i < nVars; i++ )
     {
         for ( k = i; k < nVars; k++ )
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index 92641b71..cf2beb97 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -76,6 +76,7 @@ static inline int Dau_DsdReadVar( char * p )  { if ( *p == '!' ) p++; return *p
 
 /*=== dauCanon.c ==========================================================*/
 extern unsigned      Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm );
+extern unsigned      Abc_TtCanonicizePhase( word * pTruth, int nVars );
 /*=== dauDsd.c  ==========================================================*/
 extern int *         Dau_DsdComputeMatches( char * p );
 extern int           Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char * pRes );
diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c
index d37c44b1..26edca9b 100644
--- a/src/opt/dau/dauCanon.c
+++ b/src/opt/dau/dauCanon.c
@@ -941,6 +941,105 @@ unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm )
     return uCanonPhase;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Semi-canonical form computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_TtCanonicizePhaseVar6( word * pTruth, int nVars, int v )
+{
+    int w, nWords = Abc_TtWordNum( nVars );
+    int s, nStep = 1 << (v-6);
+    assert( v >= 6 );
+    for ( w = nWords - 1, s = nWords - nStep; w > 0; w-- )
+    {
+        if ( pTruth[w-nStep] == pTruth[w] )
+        {
+            if ( w == s ) { w = s - nStep; s = w - nStep; }
+            continue;
+        }
+        if ( pTruth[w-nStep] > pTruth[w] )
+            return -1;
+        for ( ; w > 0; w-- )
+        {
+            ABC_SWAP( word, pTruth[w-nStep], pTruth[w] );
+            if ( w == s ) { w = s - nStep; s = w - nStep; }
+        }
+        assert( w == -1 );
+        return 1;
+    }
+    return 0;
+}
+static inline int Abc_TtCanonicizePhaseVar5( word * pTruth, int nVars, int v )
+{
+    int w, nWords = Abc_TtWordNum( nVars );
+    int Shift = 1 << v;
+    word Mask = s_Truths6[v];
+    assert( v < 6 );
+    for ( w = nWords - 1; w >= 0; w-- )
+    {
+        if ( ((pTruth[w] << Shift) & Mask) == (pTruth[w] & Mask) )
+            continue;
+        if ( ((pTruth[w] << Shift) & Mask) > (pTruth[w] & Mask) )
+            return -1;
+//        Extra_PrintHex( stdout, (unsigned *)pTruth, nVars ); printf("\n" );
+        for ( ; w >= 0; w-- )
+            pTruth[w] = ((pTruth[w] << Shift) & Mask) | ((pTruth[w] & Mask) >> Shift);
+//        Extra_PrintHex( stdout, (unsigned *)pTruth, nVars ); printf( " changed %d", v ), printf("\n" );
+        return 1;
+    }
+    return 0;
+}
+unsigned Abc_TtCanonicizePhase( word * pTruth, int nVars )
+{
+    unsigned uCanonPhase = 0;
+    int v, nWords = Abc_TtWordNum( nVars );
+//    static int Counter = 0;
+//    Counter++;
+
+#ifdef CANON_VERIFY
+    static word pCopy1[1024];
+    static word pCopy2[1024];
+    Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
+#endif
+
+    if ( (pTruth[nWords-1] >> 63) & 1 )
+    {
+        Abc_TtNot( pTruth, nWords );
+        uCanonPhase ^= (1 << nVars);
+    }
+
+//    while ( 1 )
+//    {
+//        unsigned uCanonPhase2 = uCanonPhase;
+        for ( v = nVars - 1; v >= 6; v-- )
+            if ( Abc_TtCanonicizePhaseVar6( pTruth, nVars, v ) == 1 )
+                uCanonPhase ^= 1 << v;
+        for ( ; v >= 0; v-- )
+            if ( Abc_TtCanonicizePhaseVar5( pTruth, nVars, v ) == 1 )
+                uCanonPhase ^= 1 << v;
+//        if ( uCanonPhase2 == uCanonPhase )
+//            break;
+//    }
+
+//    for ( v = 5; v >= 0; v-- )
+//        assert( Abc_TtCanonicizePhaseVar5( pTruth, nVars, v ) != 1 );
+
+#ifdef CANON_VERIFY
+    Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
+    Abc_TtImplementNpnConfig( pCopy2, nVars, NULL, uCanonPhase );
+    if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
+        printf( "Canonical form verification failed!\n" );
+#endif
+    return uCanonPhase;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///