Improvements to the truth table computations.

2 files changed, 19 insertions, 26 deletions

diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c
index 2853f238..34387e4d 100644
--- a/src/opt/dau/dauCanon.c
+++ b/src/opt/dau/dauCanon.c
@@ -27,6 +27,14 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static word s_CMasks6[5] = {
+    0x1111111111111111,
+    0x0303030303030303,
+    0x000F000F000F000F,
+    0x000000FF000000FF,
+    0x000000000000FFFF
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -406,8 +414,8 @@ int Abc_TtCountOnesInCofsFast6_rec( word Truth, int iVar, int nBytes, int * pSto
         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 );
+    nMints0 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cofactor0(Truth, iVar), iVar - 1, nBytes/2, pStore );
+    nMints1 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cofactor1(Truth, iVar), iVar - 1, nBytes/2, pStore );
     pStore[iVar] += nMints0;
     return nMints0 + nMints1;
 }
@@ -899,7 +907,7 @@ unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm )
 #endif
 
     uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn );
-    for ( k = 0; k < 3; k++ )
+    for ( k = 0; k < 5; k++ )
     {
         int fChanges = 0;
         for ( i = nVars - 2; i >= 0; i-- )
diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c
index d319e62d..c2cfad35 100644
--- a/src/opt/dau/dauDsd.c
+++ b/src/opt/dau/dauDsd.c
@@ -165,21 +165,6 @@ void Dau_DsdTest2()
   SeeAlso     []
 
 ***********************************************************************/
-static inline word Dau_DsdCof0( word t, int iVar )
-{
-    assert( iVar >= 0 && iVar < 6 );
-    return (t &~s_Truth6[iVar]) | ((t &~s_Truth6[iVar]) << (1<<iVar));
-}
-static inline word Dau_DsdCof1( word t, int iVar )
-{
-    assert( iVar >= 0 && iVar < 6 );
-    return (t & s_Truth6[iVar]) | ((t & s_Truth6[iVar]) >> (1<<iVar));
-}
-static inline word Dau_DsdVarPres( word t, int iVar )
-{
-    assert( iVar >= 0 && iVar < 6 );
-    return (t & s_Truth6[iVar]) != ((t << (1<<iVar)) & s_Truth6[iVar]);
-}
 static inline int Dau_DsdPerformReplace( char * pBuffer, int PosStart, int Pos, int Symb, char * pNext )
 {
     static char pTemp[DAU_MAX_STR+20];
@@ -206,7 +191,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
     // perform support minimization
     nVarsNew = 0;
     for ( v = 0; v < nVars; v++ )
-        if ( Dau_DsdVarPres( t, pVars[v] ) )
+        if ( Abc_Tt6HasVar( t, pVars[v] ) )
             pVarsNew[ nVarsNew++ ] = pVars[v];
     assert( nVarsNew > 0 );
     // special case when function is a var
@@ -229,8 +214,8 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
     // decompose on the output side
     for ( v = 0; v < nVarsNew; v++ )
     {
-        Cof0[v] = Dau_DsdCof0( t, pVarsNew[v] );
-        Cof1[v] = Dau_DsdCof1( t, pVarsNew[v] );
+        Cof0[v] = Abc_Tt6Cofactor0( t, pVarsNew[v] );
+        Cof1[v] = Abc_Tt6Cofactor1( t, pVarsNew[v] );
         assert( Cof0[v] != Cof1[v] );
         if ( Cof0[v] == 0 ) // ax
         {
@@ -281,10 +266,10 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
     for ( v = 0; v < nVarsNew; v++ )
     for ( u = v+1; u < nVarsNew; u++ )
     {
-        Cof[0] = Dau_DsdCof0( Cof0[v], pVarsNew[u] );
-        Cof[1] = Dau_DsdCof1( Cof0[v], pVarsNew[u] );
-        Cof[2] = Dau_DsdCof0( Cof1[v], pVarsNew[u] );
-        Cof[3] = Dau_DsdCof1( Cof1[v], pVarsNew[u] );
+        Cof[0] = Abc_Tt6Cofactor0( Cof0[v], pVarsNew[u] );
+        Cof[1] = Abc_Tt6Cofactor1( Cof0[v], pVarsNew[u] );
+        Cof[2] = Abc_Tt6Cofactor0( Cof1[v], pVarsNew[u] );
+        Cof[3] = Abc_Tt6Cofactor1( Cof1[v], pVarsNew[u] );
         if ( Cof[0] == Cof[1] && Cof[0] == Cof[2] ) // vu
         {
             PosStart = Pos;
@@ -333,7 +318,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
     {
         int CountCur = 0;
         for ( u = 0; u < nVarsNew; u++ )
-            if ( u != v && Dau_DsdVarPres(Cof0[v], pVarsNew[u]) && Dau_DsdVarPres(Cof1[v], pVarsNew[u]) )
+            if ( u != v && Abc_Tt6HasVar(Cof0[v], pVarsNew[u]) && Abc_Tt6HasVar(Cof1[v], pVarsNew[u]) )
                 CountCur++;
         if ( CountBest > CountCur )
         {