Merged in petkovska/abc-pullreq/hier-npn_fast-exact (pull request #29)

Exact hierarchical NPN classification

src/base/abci/abcNpn.c

@@ -181,7 +181,7 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
     char pCanonPerm[16];
     unsigned uCanonPhase=0;
     abctime clk = Abc_Clock();
-    int i, nClasses = -1;
+    int i;
 
     char * pAlgoName = NULL;
     if ( NpnType == 0 )
@@ -293,27 +293,28 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
     }
     else if ( NpnType == 7 )
     {
-        extern unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruth, int nVars, char * pCanonPerm );
+        extern unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int fExact );
         extern Abc_TtMan_t * Abc_TtManStart( int nVars );
         extern void Abc_TtManStop( Abc_TtMan_t * p );
         extern int Abc_TtManNumClasses( Abc_TtMan_t * p );
 
+        int fExact = 0;
         Abc_TtMan_t * pMan = Abc_TtManStart( p->nVars );
         for ( i = 0; i < p->nFuncs; i++ )
         {
             if ( fVerbose )
                 printf( "%7d : ", i );
-            uCanonPhase = Abc_TtCanonicizeHie( pMan, p->pFuncs[i], p->nVars, pCanonPerm );
+            uCanonPhase = Abc_TtCanonicizeHie( pMan, p->pFuncs[i], p->nVars, pCanonPerm, fExact );
             if ( fVerbose )
 //                Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(NULL, uCanonPhase, p->nVars), printf( "\n" );
                 printf( "\n" );
         }
-        nClasses = Abc_TtManNumClasses( pMan );
+        // nClasses = Abc_TtManNumClasses( pMan );
         Abc_TtManStop( pMan );
     }
     else assert( 0 );
     clk = Abc_Clock() - clk;
-    printf( "Classes =%9d  ", nClasses == -1 ? Abc_TruthNpnCountUnique(p) : nClasses );
+    printf( "Classes =%9d  ", Abc_TruthNpnCountUnique(p) );
     Abc_PrintTime( 1, "Time", clk );
 }
 

src/bool/lucky/luckySimple.c

@@ -148,6 +148,11 @@ static inline void minWord3(word* a, word* b, word* minimal, int nVars)
     if (memCompare(b, minimal, nVars) <= 0)
         Kit_TruthCopy_64bit( minimal, b, nVars );
 }
+static inline void minWord1(word* a, word* minimal, int nVars)
+{
+    if (memCompare(a, minimal, nVars) <= 0)
+        Kit_TruthCopy_64bit( minimal, a, nVars );
+}
 void simpleMinimal(word* x, word* pAux,word* minimal, permInfo* pi, int nVars)
 {
     int i,j=0;
@@ -179,5 +184,119 @@ void simpleMinimal(word* x, word* pAux,word* minimal, permInfo* pi, int nVars)
     Kit_TruthCopy_64bit( x, minimal, nVars );    
 }
 
+/**
+ * pGroups: we assume that the variables are merged into adjacent groups,
+ *          the size of each group is stored in pGroups
+ * nGroups: the number of groups
+ *
+ * pis:     we compute all permInfos from 0 to nVars (incl.)
+ */
+void simpleMinimalGroups(word* x, word* pAux, word* minimal, int* pGroups, int nGroups, permInfo** pis, int nVars, int fFlipOutput, int fFlipInput)
+{
+    /* variables */
+    int i, j, o, nn;
+    permInfo* pi;
+
+    /* reorder groups and calculate group offsets */
+    int offset[nGroups];
+    o = 0;
+    j = 0;
+
+    for ( i = 0; i < nGroups; ++i )
+    {
+        offset[j] = o;
+        o += pGroups[j];
+        ++j;
+    }
+
+    if ( fFlipOutput )
+    {
+        /* keep regular and inverted version of x */
+        Kit_TruthCopy_64bit( pAux, x, nVars );
+        Kit_TruthNot_64bit( x, nVars );
+
+        minWord(x, pAux, minimal, nVars);
+    }
+    else
+    {
+        Kit_TruthCopy_64bit( minimal, x, nVars );
+    }
+
+    /* iterate through all combinations of pGroups using mixed radix enumeration */
+    nn = ( nGroups << 1 ) + 1;
+    int a[nn];
+    int c[nn];
+    int m[nn];
+
+    /* fill a and m arrays */
+    m[0] = 2;
+    for ( i = 1; i <= nGroups; ++i ) { m[i]           = pis[pGroups[i - 1]]->totalFlips + 1; }
+    for ( i = 1; i <= nGroups; ++i ) { m[nGroups + i] = pis[pGroups[i - 1]]->totalSwaps + 1; }
+    for ( i = 0; i < nn; ++i )       { a[i] = c[i] = 0; }
+
+    while ( 1 )
+    {
+        /* consider all flips */
+        for ( i = 1; i <= nGroups; ++i )
+        {
+            if ( !c[i] ) { continue; }
+            if ( !fFlipInput && pGroups[i - 1] == 1 ) { continue; }
+
+            pi = pis[pGroups[i - 1]];
+            j = a[i] == 0 ? 0 : pi->totalFlips - a[i];
+
+            Kit_TruthChangePhase_64bit(x, nVars, offset[i - 1] + pi->flipArray[j]);
+            if ( fFlipOutput )
+            {
+                Kit_TruthChangePhase_64bit(pAux, nVars, offset[i - 1] + pi->flipArray[j]);
+                minWord3(x, pAux, minimal, nVars);
+            }
+            else
+            {
+                minWord1(x, minimal, nVars);
+            }
+        }
+
+        /* consider all swaps */
+        for ( i = 1; i <= nGroups; ++i )
+        {
+            if ( !c[nGroups + i] ) { continue; }
+            if ( pGroups[i - 1] == 1 ) { continue; }
+
+            pi = pis[pGroups[i - 1]];
+            if ( a[nGroups + i] == pi->totalSwaps )
+            {
+                j = 0;
+            }
+            else
+            {
+                j = pi->swapArray[pi->totalSwaps - a[nGroups + i] - 1];
+            }
+            Kit_TruthSwapAdjacentVars_64bit(x, nVars, offset[i - 1] + j);
+            if ( fFlipOutput )
+            {
+                Kit_TruthSwapAdjacentVars_64bit(pAux, nVars, offset[i - 1] + j);
+                minWord3(x, pAux, minimal, nVars);
+            }
+            else
+            {
+                minWord1(x, minimal, nVars);
+            }
+        }
+
+        /* update a's */
+        memset(c, 0, sizeof(int) * nn);
+        j = nn - 1;
+        while ( a[j] == m[j] - 1 ) { c[j] = 1; a[j--] = 0; }
+
+        /* done? */
+        if ( j == 0 ) { break; }
+
+        c[j] = 1;
+        a[j]++;
+    }
+
+    Kit_TruthCopy_64bit( x, minimal, nVars );
+}
 
 ABC_NAMESPACE_IMPL_END

src/opt/dau/dauCanon.c

@@ -21,6 +21,7 @@
 #include "dauInt.h"
 #include "misc/util/utilTruth.h"
 #include "misc/vec/vecMem.h"
+#include "bool/lucky/lucky.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -1053,13 +1054,32 @@ unsigned Abc_TtCanonicizePhase( word * pTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-#define TT_NUM_TABLES 4
+#define TT_NUM_TABLES 5
 
 struct Abc_TtMan_t_
 {
     Vec_Mem_t *   vTtMem[TT_NUM_TABLES];   // truth table memory and hash tables
+    Vec_Int_t **  vRepres;                 // pointers to the representatives from the last hierarchical level
 };
 
+Vec_Int_t ** Abc_TtRepresStart() {
+    Vec_Int_t ** vRepres = ABC_ALLOC(Vec_Int_t *, TT_NUM_TABLES - 1);
+    int i;
+    // create a list of pointers for each level of the hierarchy
+    for (i = 0; i < (TT_NUM_TABLES - 1); i++) {
+        vRepres[i] = Vec_IntAlloc(1);
+    }
+    return vRepres;
+}
+
+void Abc_TtRepresStop(Vec_Int_t ** vRepres) {
+    int i;
+    for (i = 0; i < (TT_NUM_TABLES - 1); i++) {
+        Vec_IntFree(vRepres[i]);
+    }
+    ABC_FREE( vRepres );
+}
+
 Abc_TtMan_t * Abc_TtManStart( int nVars )
 {
     Abc_TtMan_t * p = ABC_CALLOC( Abc_TtMan_t, 1 );
@@ -1069,6 +1089,7 @@ Abc_TtMan_t * Abc_TtManStart( int nVars )
         p->vTtMem[i] = Vec_MemAlloc( nWords, 12 );
         Vec_MemHashAlloc( p->vTtMem[i], 10000 );
     }
+    p->vRepres = Abc_TtRepresStart();
     return p;
 }
 void Abc_TtManStop( Abc_TtMan_t * p )
@@ -1079,6 +1100,7 @@ void Abc_TtManStop( Abc_TtMan_t * p )
         Vec_MemHashFree( p->vTtMem[i] );
         Vec_MemFreeP( &p->vTtMem[i] );
     }
+    Abc_TtRepresStop(p->vRepres);
     ABC_FREE( p );
 }
 int Abc_TtManNumClasses( Abc_TtMan_t * p )
@@ -1086,7 +1108,7 @@ int Abc_TtManNumClasses( Abc_TtMan_t * p )
     return Vec_MemEntryNum( p->vTtMem[TT_NUM_TABLES-1] );
 }
 
-unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, char * pCanonPerm )
+unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, char * pCanonPerm, int fExact )
 {
     int fNaive = 1;
     int pStore[17];
@@ -1095,6 +1117,9 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha
     int nOnes, nWords = Abc_TtWordNum( nVars );
     int i, k, truthId;
     int * pSpot;
+    int vTruthId[TT_NUM_TABLES-1];
+    int fLevelFound;
+    word * pRepTruth;
     assert( nVars <= 16 );
 
     Abc_TtCopy( pTruth, pTruthInit, nWords, 0 );
@@ -1112,9 +1137,11 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha
     }
     // check cache
     pSpot = Vec_MemHashLookup( p->vTtMem[0], pTruth );
-    if ( *pSpot != -1 )
-        return 0;
-    truthId = Vec_MemHashInsert( p->vTtMem[0], pTruth );
+    if ( *pSpot != -1 ) {
+        fLevelFound = 0;
+        goto end_repres;
+    }
+    vTruthId[0] = Vec_MemHashInsert( p->vTtMem[0], pTruth );
 
     // normalize phase
     Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
@@ -1129,9 +1156,11 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha
     }
     // check cache
     pSpot = Vec_MemHashLookup( p->vTtMem[1], pTruth );
-    if ( *pSpot != -1 )
-        return 0;
-    truthId = Vec_MemHashInsert( p->vTtMem[1], pTruth );
+    if ( *pSpot != -1 ) {
+        fLevelFound = 1;
+        goto end_repres;
+    }
+    vTruthId[1] = Vec_MemHashInsert( p->vTtMem[1], pTruth );
 
     // normalize permutation
     {
@@ -1156,9 +1185,11 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha
     }
     // check cache
     pSpot = Vec_MemHashLookup( p->vTtMem[2], pTruth );
-    if ( *pSpot != -1 )
-        return 0;
-    truthId = Vec_MemHashInsert( p->vTtMem[2], pTruth );
+    if ( *pSpot != -1 ) {
+        fLevelFound = 2;
+        goto end_repres;
+    }
+    vTruthId[2] = Vec_MemHashInsert( p->vTtMem[2], pTruth );
 
     // iterate TT permutations for tied variables
     for ( k = 0; k < 5; k++ )
@@ -1178,9 +1209,69 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha
     }
     // check cache
     pSpot = Vec_MemHashLookup( p->vTtMem[3], pTruth );
-    if ( *pSpot != -1 )
-        return 0;
-    truthId = Vec_MemHashInsert( p->vTtMem[3], pTruth );
+    if ( *pSpot != -1 ) {
+        fLevelFound = 3;
+        goto end_repres;
+    }
+    vTruthId[3] = Vec_MemHashInsert( p->vTtMem[3], pTruth );
+
+    // perform exact NPN using groups
+    if ( fExact ) {
+        extern void simpleMinimalGroups(word* x, word* pAux, word* minimal, int* pGroups, int nGroups, permInfo** pis, int nVars, int fFlipOutput, int fFlipInput);
+        word pAuxWord[1024], pAuxWord1[1024];
+        int pGroups[nVars];
+        int nGroups = 0;
+        // get groups
+        pGroups[0] = 0;
+        for (i = 0; i < nVars - 1; i++) {
+            if (pStore[i] == pStore[i + 1]) {
+                pGroups[nGroups]++;
+            } else {
+                pGroups[nGroups]++;
+                nGroups++;
+                pGroups[nGroups] = 0;
+            }
+        }
+        pGroups[nGroups]++;
+        nGroups++;
+
+        // compute permInfo from 0 to nVars  (incl.)
+        permInfo * pis[nVars+1];
+        for (i = 0; i <= nVars; i++) {
+            pis[i] = setPermInfoPtr(i);
+        }
+
+        // do the exact matching
+        if (nOnes == nWords * 32) /* balanced output */
+            simpleMinimalGroups(pTruth, pAuxWord, pAuxWord1, pGroups, nGroups, pis, nVars, 1, 1);
+        else if (pStore[0] != pStore[1] && pStore[0] == (nOnes - pStore[0])) /* balanced singleton input */
+            simpleMinimalGroups(pTruth, pAuxWord, pAuxWord1, pGroups, nGroups, pis, nVars, 0, 1);
+        else
+            simpleMinimalGroups(pTruth, pAuxWord, pAuxWord1, pGroups, nGroups, pis, nVars, 0, 0);
+
+        // cleanup
+        for (i = 0; i <= nVars; i++) {
+            freePermInfoPtr(pis[i]);
+        }
+    }
+    // check cache
+    pSpot = Vec_MemHashLookup( p->vTtMem[4], pTruth );
+    fLevelFound = 4;
+    if ( *pSpot != -1 ) {
+        goto end_repres;
+    }
+    *pSpot = Vec_MemHashInsert( p->vTtMem[4], pTruth );
+
+end_repres:
+    // return the class representative
+    if(fLevelFound < (TT_NUM_TABLES - 1))
+        truthId = Vec_IntEntry(p->vRepres[fLevelFound], *pSpot);
+    else truthId = *pSpot;
+    for(i = 0; i < fLevelFound; i++)
+        Vec_IntSetEntry(p->vRepres[i], vTruthId[i], truthId);
+    pRepTruth = Vec_MemReadEntry(p->vTtMem[TT_NUM_TABLES-1], truthId);
+    Abc_TtCopy( pTruthInit, pRepTruth, nWords, 0 );
+
     return 0;
 }