Improvements to the truth table computations.

src/misc/util/utilTruth.h

@@ -81,6 +81,7 @@ static word s_CMasks6[5] = {
 
 ***********************************************************************/
 static inline int  Abc_TtWordNum( int nVars ) { return nVars <= 6 ? 1 : 1 << (nVars-6); }
+static inline int  Abc_TtByteNum( int nVars ) { return nVars <= 3 ? 1 : 1 << (nVars-3); }
 
 /**Function*************************************************************
 
@@ -143,6 +144,22 @@ static inline int Abc_TtCompareRev( word * pIn1, word * pIn2, int nWords )
             return (pIn1[w] < pIn2[w]) ? -1 : 1;
     return 0;
 }
+static inline int Abc_TtIsConst0( word * pIn1, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        if ( pIn1[w] )
+            return 0;
+    return 1;
+}
+static inline int Abc_TtIsConst1( word * pIn1, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        if ( ~pIn1[w] )
+            return 0;
+    return 1;
+}
 
  
 /**Function*************************************************************
@@ -500,6 +517,17 @@ static inline int Abc_Tt6Cof1IsConst0( word t, int iVar ) { return (t & s_Truths
 static inline int Abc_Tt6Cof1IsConst1( word t, int iVar ) { return (t & s_Truths6[iVar]) == s_Truths6[iVar];                               }
 static inline int Abc_Tt6CofsOpposite( word t, int iVar ) { return ((t >> (1 << iVar)) & s_Truths6Neg[iVar]) == (~t & s_Truths6Neg[iVar]); } 
 
+static inline word Abc_Tt6Cof0( word t, int iVar )
+{
+    assert( iVar >= 0 && iVar < 6 );
+    return (t &s_Truths6Neg[iVar]) | ((t &s_Truths6Neg[iVar]) << (1<<iVar));
+}
+static inline word Abc_Tt6Cof1( word t, int iVar )
+{
+    assert( iVar >= 0 && iVar < 6 );
+    return (t & s_Truths6[iVar]) | ((t & s_Truths6[iVar]) >> (1<<iVar));
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -1073,7 +1101,10 @@ static inline void Abc_TtCountOnesInCofsSlow( word * pTruth, int nVars, int * pS
 ***********************************************************************/
 static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm )
 {
+    extern int Abc_TtCountOnesInCofsFast( word * pTruth, int nVars, int * pStore );
+
     int pStore[16];
+//    int pStore2[16];
     int nWords = Abc_TtWordNum( nVars );
     int i, k, BestK, Temp, nOnes;//, nSwaps = 0;//, fChange;
     unsigned  uCanonPhase = 0;
@@ -1087,8 +1118,13 @@ static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pC
         uCanonPhase |= (1 << nVars);
     }
     // normalize phase
-//    Abc_TtCountOnesInCofsSlow( pTruth, nVars, pStore );
-    Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
+//    Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
+    Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore );
+
+//    Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore2 );
+//    for ( i = 0; i < nVars; i++ )
+//        assert( pStore[i] == pStore2[i] );
+
     for ( i = 0; i < nVars; i++ )
     {
         if ( pStore[i] >= nOnes - pStore[i] )

src/opt/dau/dauCanon.c

@@ -526,6 +526,93 @@ void Abc_TtConfactorTest( word * pTruth, int nVars, int N )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_TtCountOnesInCofsFast6_rec( word Truth, int iVar, int nBytes, int * pStore )
+{
+    static int bit_count[256] = {
+      0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
+      1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+      1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+      2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+      1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+      2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+      2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+      3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
+    };
+    int nMints0, nMints1;
+    if ( Truth == 0 )
+        return 0;
+    if ( ~Truth == 0 )
+    {
+        int i;
+        for ( i = 0; i <= iVar; i++ )
+            pStore[i] += nBytes * 4;
+        return nBytes * 8;
+    }
+    if ( nBytes == 1 )
+    {
+        assert( iVar == 2 );
+        pStore[0] += bit_count[ Truth & 0x55 ];
+        pStore[1] += bit_count[ Truth & 0x33 ];
+        pStore[2] += bit_count[ Truth & 0x0F ];
+        return bit_count[ Truth & 0xFF ];
+    }
+    nMints0 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cof0(Truth, iVar), iVar - 1, nBytes/2, pStore );
+    nMints1 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cof1(Truth, iVar), iVar - 1, nBytes/2, pStore );
+    pStore[iVar] += nMints0;
+    return nMints0 + nMints1;
+}
+
+int Abc_TtCountOnesInCofsFast_rec( word * pTruth, int iVar, int nWords, int * pStore )
+{
+    int nMints0, nMints1;
+    if ( nWords == 1 )
+    {
+        assert( iVar == 5 );
+        return Abc_TtCountOnesInCofsFast6_rec( pTruth[0], iVar, 8, pStore );
+    }
+    assert( nWords > 1 );
+    assert( iVar > 5 );
+    if ( pTruth[0] & 1 )
+    {
+        if ( Abc_TtIsConst1( pTruth, nWords ) )
+        {
+            int i;
+            for ( i = 0; i <= iVar; i++ )
+                pStore[i] += nWords * 32;
+            return nWords * 64;
+        }
+    }
+    else 
+    {
+        if ( Abc_TtIsConst0( pTruth, nWords ) )
+            return 0;
+    }
+    nMints0 = Abc_TtCountOnesInCofsFast_rec( pTruth,            iVar - 1, nWords/2, pStore );
+    nMints1 = Abc_TtCountOnesInCofsFast_rec( pTruth + nWords/2, iVar - 1, nWords/2, pStore );
+    pStore[iVar] += nMints0;
+    return nMints0 + nMints1;
+}
+int Abc_TtCountOnesInCofsFast( word * pTruth, int nVars, int * pStore )
+{
+    memset( pStore, 0, sizeof(int) * nVars );
+    assert( nVars >= 3 );
+    if ( nVars <= 6 )
+        return Abc_TtCountOnesInCofsFast6_rec( pTruth[0], nVars - 1, Abc_TtByteNum( nVars ), pStore );
+    else
+        return Abc_TtCountOnesInCofsFast_rec( pTruth, nVars - 1, Abc_TtWordNum( nVars ), pStore );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///